--- a/Nominal/nominal_function_core.ML	Mon Jan 09 10:45:12 2012 +0000
+++ b/Nominal/nominal_function_core.ML	Mon Jan 16 12:42:47 2012 +0000
@@ -143,14 +143,14 @@
 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 
   mk_eqvt_at (fvar, arg)
   |> curry Logic.list_implies (map prop_of assms)
-  |> curry Term.list_all_free vs
+  |> fold_rev (Logic.all o Free) vs
   |> 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
+  |> fold_rev (Logic.all o Free) vs
   |> fold_rev absfree qs
   |> strip_abs_body
 
@@ -173,7 +173,7 @@
         |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *)
         |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *)
         |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *)
-        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
+        |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs')
         |> curry abstract_over fvar
         |> curry subst_bound f
       end
@@ -535,7 +535,7 @@
     val thy = Proof_Context.theory_of ctxt
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
+    val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
@@ -760,7 +760,7 @@
       |> cterm_of thy
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
+    val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (P $ Bound 0)))
       |> cterm_of thy
@@ -940,7 +940,7 @@
       |> cterm_of thy (* "wf R'" *)
 
     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
+    val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
       |> cterm_of thy