--- a/Nominal/nominal_function_core.ML	Thu Aug 18 14:10:52 2011 +0200
+++ b/Nominal/nominal_function_core.ML	Fri Aug 19 10:56:12 2011 +0900
@@ -144,14 +144,14 @@
   mk_eqvt_at (fvar, arg)
   |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_all_free vs
-  |> curry Term.list_abs_free qs
+  |> fold_rev absfree qs
   |> strip_abs_body
 
 fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = 
   mk_inv inv (fvar, arg)
   |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_all_free vs
-  |> curry Term.list_abs_free qs
+  |> fold_rev absfree qs
   |> strip_abs_body
 
 (** building proof obligations *)

--- a/Nominal/nominal_inductive.ML	Thu Aug 18 14:10:52 2011 +0200
+++ b/Nominal/nominal_inductive.ML	Fri Aug 19 10:56:12 2011 +0900
@@ -104,7 +104,7 @@
       |> map (add_c_prop true Ps (Bound 0, c_name, c_ty))
 
     val avoid_trm' = avoid_trm
-      |> (curry list_abs_free) (params @ [(c_name, c_ty)])
+      |> fold_rev absfree (params @ [(c_name, c_ty)])
       |> strip_abs_body
       |> (fn t => mk_fresh_star_ty c_ty t (Bound 0))
       |> HOLogic.mk_Trueprop
@@ -439,4 +439,4 @@
       Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd)
 end
 
-end
\ No newline at end of file
+end