# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1326717767 0
# Node ID 61db5ad429bbc54cef693b43ce3758244ee3afe6
# Parent  e26e933efba0253e8d88dd92979b99edbd9c2d79
updated to Isabelle 16 January

diff -r e26e933efba0 -r 61db5ad429bb Nominal/nominal_basics.ML
--- a/Nominal/nominal_basics.ML	Mon Jan 09 10:45:12 2012 +0000
+++ b/Nominal/nominal_basics.ML	Mon Jan 16 12:42:47 2012 +0000
@@ -140,7 +140,7 @@
 
 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
 
-fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
+fun mk_all (a, T) t =  Logic.all_const T $ Abs (a, T, t)
 
 fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)
 
diff -r e26e933efba0 -r 61db5ad429bb Nominal/nominal_function_core.ML
--- 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
diff -r e26e933efba0 -r 61db5ad429bb Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Mon Jan 09 10:45:12 2012 +0000
+++ b/Nominal/nominal_inductive.ML	Mon Jan 16 12:42:47 2012 +0000
@@ -46,12 +46,12 @@
       |> mk_fresh_star avoid_trm 
       |> HOLogic.mk_Trueprop
       |> (curry Logic.list_implies) prems
-      |> (curry list_all_free) params
+      |> fold_rev (Logic.all o Free) params
     val finite_goal = avoid_trm
       |> mk_finite
       |> HOLogic.mk_Trueprop
       |> (curry Logic.list_implies) prems
-      |> (curry list_all_free) params
+      |> fold_rev (Logic.all o Free) params
   in 
     if null avoid then [] else [vc_goal, finite_goal]
   end