# HG changeset patch
# User wenzelm
# Date 1214257539 -7200
# Node ID 1af2598b5f7d419e045f3afca1c4647c44d3baed
# Parent  91c0c894e1b4ce01b9f551163b02f7fde5a6acbb
Logic.all/mk_equals/mk_implies;

diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Fun.thy	Mon Jun 23 23:45:39 2008 +0200
@@ -509,7 +509,7 @@
       case find_double t of
         (T, NONE) => NONE
       | (T, SOME rhs) =>
-          SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs)
+          SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
             (fn _ =>
               rtac eq_reflection 1 THEN
               rtac ext 1 THEN
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy	Mon Jun 23 23:45:39 2008 +0200
@@ -305,8 +305,7 @@
                          (Free ("P",varsT --> boolT) $ mk_bodyC vars));
                    val small_Collect = mk_CollectC (Abs("x",varsT,
                            Free ("P",varsT --> boolT) $ Bound 0));
-                   val impl = implies $ (Mset_incl big_Collect) $ 
-                                          (Mset_incl small_Collect);
+                   val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -72,8 +72,7 @@
                          (Free ("P",varsT --> boolT) $ mk_bodyC vars));
                    val small_Collect = mk_CollectC (Abs("x",varsT,
                            Free ("P",varsT --> boolT) $ Bound 0));
-                   val impl = implies $ (Mset_incl big_Collect) $ 
-                                          (Mset_incl small_Collect);
+                   val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -159,13 +159,15 @@
         val cert = cterm_of Pure.thy
         val xT = TFree("'a",[])
         val yT = TFree("'b",[])
+        val x = Free("x",xT)
+        val y = Free("y",yT)
         val P = Free("P",xT-->yT-->propT)
-        val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
-        val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
+        val lhs = Logic.all x (Logic.all y (P $ x $ y))
+        val rhs = Logic.all y (Logic.all x (P $ x $ y))
         val cl = cert lhs
         val cr = cert rhs
-        val cx = cert (Free("x",xT))
-        val cy = cert (Free("y",yT))
+        val cx = cert x
+        val cy = cert y
         val th1 = assume cr
                          |> forall_elim_list [cy,cx]
                          |> forall_intr_list [cx,cy]
@@ -415,6 +417,8 @@
 fun mk_free s t = Free (s,t)
 val xT = mk_tfree "a"
 val yT = mk_tfree "b"
+val x = Free ("x", xT)
+val y = Free ("y", yT)
 val P  = mk_free "P" (xT-->yT-->propT)
 val Q  = mk_free "Q" (xT-->yT)
 val R  = mk_free "R" (xT-->yT)
@@ -436,7 +440,7 @@
 fun quant_simproc thy = Simplifier.simproc_i
                            thy
                            "Ordered rewriting of nested quantifiers"
-                           [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
+                           [Logic.all x (Logic.all y (P $ x $ y))]
                            quant_rewrite
 fun eta_expand_simproc thy = Simplifier.simproc_i
                          thy
@@ -446,7 +450,7 @@
 fun eta_contract_simproc thy = Simplifier.simproc_i
                          thy
                          "Smart handling of eta-contractions"
-                         [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
+                         [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
                          eta_contract
 end
 
@@ -582,8 +586,7 @@
 fun set_prop thy t =
     let
         val vars = add_term_frees (t,add_term_vars (t,[]))
-        val closed_t = Library.foldr (fn (v, body) =>
-      let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
+        val closed_t = fold_rev Logic.all vars t
         val rew_th = norm_term thy closed_t
         val rhs = Thm.rhs_of rew_th
 
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -251,7 +251,7 @@
                (trm,trm',vars,_,true)
                 => let
                      val eq1 = Goal.prove ctxt [] [] 
-                                      (list_all (vars,equals sT$trm$trm'))
+                                      (list_all (vars, Logic.mk_equals (trm, trm')))
                                       (fn _ => rtac meta_ext 1 THEN 
                                                simp_tac ss1 1);
                      val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -637,8 +637,8 @@
   let
     val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
   in
-    equals propT $ HOLogic.mk_Trueprop t $
-      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
+    Logic.mk_equals (HOLogic.mk_Trueprop t,
+      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
   end;
 
 end;
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -237,8 +237,8 @@
         val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
         val lhs = list_comb (Const (cname, constrT), l_args);
         val rhs = mk_univ_inj r_args n i;
-        val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
-        val def_name = (Sign.base_name cname) ^ "_def";
+        val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
+        val def_name = Sign.base_name cname ^ "_def";
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
         val ([def_thm], thy') =
@@ -346,8 +346,8 @@
         val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
         val fTs = map fastype_of fs;
         val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
-          equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
-            list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
+          Logic.mk_equals (Const (iso_name, T --> Univ_elT),
+            list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
         val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
 
         (* prove characteristic equations *)
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -177,7 +177,7 @@
 
 fun export_term (fixes, assumes) =
     fold_rev (curry Logic.mk_implies o prop_of) assumes 
- #> fold_rev (mk_forall o Free) fixes
+ #> fold_rev (Logic.all o Free) fixes
 
 fun export_thm thy (fixes, assumes) =
     fold_rev (implies_intr o cprop_of) assumes
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -152,7 +152,7 @@
         fun mk_assum qs pats = 
             HOLogic.mk_Trueprop P
             |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
-            |> fold_rev mk_forall qs
+            |> fold_rev Logic.all qs
             |> cterm_of thy
 
         val hyps = map2 mk_assum qss patss
@@ -221,7 +221,7 @@
             HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
                           Const ("HOL.undefined", rT))
               |> HOLogic.mk_Trueprop
-              |> fold_rev mk_forall qs
+              |> fold_rev Logic.all qs
           end
     in
       map mk_eqn fixes
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -21,9 +21,6 @@
 fun plural sg pl [x] = sg
   | plural sg pl _ = pl
 
-(* ==> logic.ML? *)
-fun mk_forall v t = all (fastype_of v) $ lambda v t
-
 (* lambda-abstracts over an arbitrarily nested tuple
   ==> hologic.ML? *)
 fun tupled_lambda vars t =
@@ -117,7 +114,7 @@
   | rename_bound n _ = raise Match
 
 fun mk_forall_rename (n, v) =
-    rename_bound n o mk_forall v 
+    rename_bound n o Logic.all v 
 
 val dummy_term = Free ("", dummyT)
 
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/induction_scheme.ML
--- a/src/HOL/Tools/function_package/induction_scheme.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/induction_scheme.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -146,7 +146,7 @@
       HOLogic.mk_Trueprop Pbool
        |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
        |> fold_rev (curry Logic.mk_implies) Cs'
-       |> fold_rev (mk_forall o Free) ws
+       |> fold_rev (Logic.all o Free) ws
        |> fold_rev mk_forall_rename (map fst xs ~~ xs')
        |> mk_forall_rename ("P", Pbool)
     end
@@ -169,7 +169,7 @@
             val cse = 
                 HOLogic.mk_Trueprop thesis
                 |> fold_rev (curry Logic.mk_implies) Cs'
-                |> fold_rev (mk_forall o Free) ws
+                |> fold_rev (Logic.all o Free) ws
           in
             Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
           end
@@ -180,7 +180,7 @@
                 let val export = 
                          fold_rev (curry Logic.mk_implies) Gas
                          #> fold_rev (curry Logic.mk_implies) gs
-                         #> fold_rev (mk_forall o Free) Gvs
+                         #> fold_rev (Logic.all o Free) Gvs
                          #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
                 in
                 (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
@@ -188,7 +188,7 @@
                  |> export,
                  mk_pres bidx' rcarg
                  |> export
-                 |> mk_forall thesis)
+                 |> Logic.all thesis)
                 end
           in
             map g rs
@@ -205,7 +205,7 @@
       fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
           HOLogic.mk_Trueprop (list_comb (P, map Free xs))
           |> fold_rev (curry Logic.mk_implies) Cs
-          |> fold_rev (mk_forall o Free) ws
+          |> fold_rev (Logic.all o Free) ws
           |> term_conv thy ind_atomize
           |> ObjectLogic.drop_judgment thy
           |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
@@ -230,13 +230,13 @@
       val P_comp = mk_ind_goal thy branches
 
       (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-      val ihyp = all T $ Abs ("z", T, 
-               implies $ 
-                  HOLogic.mk_Trueprop (
+      val ihyp = Term.all T $ Abs ("z", T, 
+               Logic.mk_implies
+                 (HOLogic.mk_Trueprop (
                   Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
                     $ (HOLogic.pair_const T T $ Bound 0 $ x) 
-                    $ R)
-             $ HOLogic.mk_Trueprop (P_comp $ Bound 0))
+                    $ R),
+                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
            |> cert
 
       val aihyp = assume ihyp
@@ -290,7 +290,7 @@
                   val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
                              |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
                              |> fold_rev (curry Logic.mk_implies) gs
-                             |> fold_rev (mk_forall o Free) qs
+                             |> fold_rev (Logic.all o Free) qs
                              |> cert
                              
                   val Plhs_to_Pxs_conv = 
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -70,8 +70,7 @@
     let
       val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
     in
-      Logic.list_implies (prems, concl)
-        |> fold_rev FundefLib.mk_forall vars
+      fold_rev Logic.all vars (Logic.list_implies (prems, concl))
     end
 
 fun prove thy solve_tac t =
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -101,7 +101,7 @@
           let
             val t = Pattern.rewrite_term thy sigma [] feq1
           in
-            fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
+            fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
           end
     in
       map instantiate substs
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -29,14 +29,10 @@
     val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
   in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
 
-fun forall_intr_prf (t, prf) =
+fun forall_intr_prf t prf =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
 
-fun forall_intr_term (t, u) =
-  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
-  in all T $ Abs (a, T, abstract_over (t, u)) end;
-
 fun subsets [] = [[]]
   | subsets (x::xs) =
       let val ys = subsets xs
@@ -264,13 +260,13 @@
     val rlzvs = rev (Term.add_vars (prop_of rrule) []);
     val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
     val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
-    val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
-    val rlz'' = foldr forall_intr_term rlz vs2
+    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
+    val rlz'' = fold_rev Logic.all vs2 rlz
   in (name, (vs,
     if rt = Extraction.nullt then rt else
       foldr (uncurry lambda) rt vs1,
     ProofRewriteRules.un_hhf_proof rlz' rlz''
-      (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
+      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
   end;
 
 fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
@@ -427,7 +423,7 @@
       let
         val (prem :: prems) = prems_of elim;
         fun reorder1 (p, (_, intr)) =
-          Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
+          Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
             (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
         fun reorder2 ((ivs, intr), i) =
           let val fs = Term.add_vars (prop_of intr) [] \\ params'
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -69,7 +69,7 @@
       fun close p t f =
         let val vs = Term.add_vars t []
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
-          (p (fold (fn x as (_, T) => fn u => all T $ lambda (Var x) u) vs t) f)
+          (p (fold (Logic.all o Var) vs t) f)
         end;
       fun mkop "op &" T x = SOME (Const ("op Int", T --> T --> T), x)
         | mkop "op |" T x = SOME (Const ("op Un", T --> T --> T), x)
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -1050,7 +1050,7 @@
               (case mk_eq_terms (upd$k$r) of
                  SOME (trm,trm',vars)
                  => SOME (prove_split_simp thy ss domS
-                                 (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
+                                 (list_all(vars, Logic.mk_equals (sel $ trm, trm'))))
                | NONE => NONE)
             end
           | NONE => NONE)
@@ -1187,7 +1187,7 @@
                Inter (trm,trm',vars,_,_)
                 => SOME (normalize_rhs 
                           (prove_split_simp thy ss rT
-                            (list_all(vars,(equals rT$trm$trm')))))
+                            (list_all(vars, Logic.mk_equals (trm, trm')))))
              | _ => NONE)
          end
        | _ => NONE))
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -86,7 +86,7 @@
                     (*Forms a lambda-abstraction over the formal parameters*)
             val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
             val cdef = cname ^ "_def"
-            val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
+            val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
       | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
@@ -113,7 +113,7 @@
                 val rhs = list_abs_free (map dest_Free args,
                                          HOLogic.choice_const T $ xtp)
                       (*Forms a lambda-abstraction over the formal parameters*)
-                val def = equals cT $ c $ rhs
+                val def = Logic.mk_equals (c, rhs)
             in dec_sko (subst_bound (list_comb(c,args), p))
                        (def :: defs)
             end
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -250,12 +250,7 @@
     singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
   end;
 
-(*Quantification over a list of Vars. FIXME: for term.ML??*)
-fun list_all_var ([], t: term) = t
-  | list_all_var ((v as Var(ix,T)) :: vars, t) =
-      (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
-
-fun gen_all_vars t = list_all_var (term_vars t, t);
+fun gen_all_vars t = fold_rev Logic.all (term_vars t) t;
 
 fun ints_of_stree_aux (Int n, ns) = n::ns
   | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -128,10 +128,6 @@
 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
 fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
 
-fun forall_intr (t, prop) =
-  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
-  in all T $ Abs (a, T, abstract_over (t, prop)) end;
-
 fun forall_intr_prf (t, prf) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   in Abst (a, SOME T, prf_abstract_over t prf) end;
@@ -324,7 +320,7 @@
         (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
           (Const ("realizes", T --> propT --> propT) $
             (if T = nullT then t else list_comb (t, vars')) $ prop);
-      val r = List.foldr forall_intr r' (map (get_var_type r') vars);
+      val r = fold_rev Logic.all (map (get_var_type r') vars) r';
       val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
     in (name, (vs, (t, prf))) end
   end;
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -26,11 +26,7 @@
 fun vars_of t = rev (fold_aterms
   (fn v as Var _ => insert (op =) v | _ => I) t []);
 
-fun forall_intr t prop =
-  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
-  in all T $ Abs (a, T, abstract_over (t, prop)) end;
-
-fun forall_intr_vfs prop = fold_rev forall_intr
+fun forall_intr_vfs prop = fold_rev Logic.all
   (vars_of prop @ sort Term.term_ord (term_frees prop)) prop;
 
 fun forall_intr_prf t prf =
@@ -317,7 +313,7 @@
 
 fun prop_of0 Hs (PBound i) = List.nth (Hs, i)
   | prop_of0 Hs (Abst (s, SOME T, prf)) =
-      all T $ (Abs (s, T, prop_of0 Hs prf))
+      Term.all T $ (Abs (s, T, prop_of0 Hs prf))
   | prop_of0 Hs (AbsP (s, SOME t, prf)) =
       Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
   | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
diff -r 91c0c894e1b4 -r 1af2598b5f7d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/Pure/proofterm.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -774,13 +774,10 @@
    ("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))),
    ("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))),
    ("equal_elim", list_implies ([mk_equals (A, B), A], B)),
-   ("abstract_rule", Logic.mk_implies
-      (all aT $ Abs ("x", aT, equals bT $ (f $ Bound 0) $ (g $ Bound 0)),
-       equals (aT --> bT) $
-         Abs ("x", aT, f $ Bound 0) $ Abs ("x", aT, g $ Bound 0))),
-   ("combination", Logic.list_implies
-      ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)],
-       Logic.mk_equals (f $ x, g $ y)))];
+   ("abstract_rule", mk_implies
+      (all x (mk_equals (f $ x, g $ x)), mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+   ("combination", list_implies
+      ([mk_equals (f, g), mk_equals (x, y)], mk_equals (f $ x, g $ y)))];
 
 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
   equal_elim_axm, abstract_rule_axm, combination_axm] =