diff -r 38147e67196e -r 4ee772b12032 Nominal/nominal_function_core.ML
--- 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 *)