Logic.all/mk_equals/mk_implies;
authorwenzelm
Mon Jun 23 23:45:39 2008 +0200 (2008-06-23)
changeset 273301af2598b5f7d
parent 27329 91c0c894e1b4
child 27331 5c66afff695e
Logic.all/mk_equals/mk_implies;
src/HOL/Fun.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Import/shuffler.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/induction_scheme.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_reconstruct.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/proofterm.ML
     1.1 --- a/src/HOL/Fun.thy	Mon Jun 23 20:00:58 2008 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Jun 23 23:45:39 2008 +0200
     1.3 @@ -509,7 +509,7 @@
     1.4        case find_double t of
     1.5          (T, NONE) => NONE
     1.6        | (T, SOME rhs) =>
     1.7 -          SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs)
     1.8 +          SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
     1.9              (fn _ =>
    1.10                rtac eq_reflection 1 THEN
    1.11                rtac ext 1 THEN
     2.1 --- a/src/HOL/Hoare/HoareAbort.thy	Mon Jun 23 20:00:58 2008 +0200
     2.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Mon Jun 23 23:45:39 2008 +0200
     2.3 @@ -305,8 +305,7 @@
     2.4                           (Free ("P",varsT --> boolT) $ mk_bodyC vars));
     2.5                     val small_Collect = mk_CollectC (Abs("x",varsT,
     2.6                             Free ("P",varsT --> boolT) $ Bound 0));
     2.7 -                   val impl = implies $ (Mset_incl big_Collect) $ 
     2.8 -                                          (Mset_incl small_Collect);
     2.9 +                   val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    2.10     in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    2.11  
    2.12  end;
     3.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 23 20:00:58 2008 +0200
     3.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 23 23:45:39 2008 +0200
     3.3 @@ -72,8 +72,7 @@
     3.4                           (Free ("P",varsT --> boolT) $ mk_bodyC vars));
     3.5                     val small_Collect = mk_CollectC (Abs("x",varsT,
     3.6                             Free ("P",varsT --> boolT) $ Bound 0));
     3.7 -                   val impl = implies $ (Mset_incl big_Collect) $ 
     3.8 -                                          (Mset_incl small_Collect);
     3.9 +                   val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    3.10     in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    3.11  
    3.12  end;
     4.1 --- a/src/HOL/Import/shuffler.ML	Mon Jun 23 20:00:58 2008 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Mon Jun 23 23:45:39 2008 +0200
     4.3 @@ -159,13 +159,15 @@
     4.4          val cert = cterm_of Pure.thy
     4.5          val xT = TFree("'a",[])
     4.6          val yT = TFree("'b",[])
     4.7 +        val x = Free("x",xT)
     4.8 +        val y = Free("y",yT)
     4.9          val P = Free("P",xT-->yT-->propT)
    4.10 -        val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
    4.11 -        val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
    4.12 +        val lhs = Logic.all x (Logic.all y (P $ x $ y))
    4.13 +        val rhs = Logic.all y (Logic.all x (P $ x $ y))
    4.14          val cl = cert lhs
    4.15          val cr = cert rhs
    4.16 -        val cx = cert (Free("x",xT))
    4.17 -        val cy = cert (Free("y",yT))
    4.18 +        val cx = cert x
    4.19 +        val cy = cert y
    4.20          val th1 = assume cr
    4.21                           |> forall_elim_list [cy,cx]
    4.22                           |> forall_intr_list [cx,cy]
    4.23 @@ -415,6 +417,8 @@
    4.24  fun mk_free s t = Free (s,t)
    4.25  val xT = mk_tfree "a"
    4.26  val yT = mk_tfree "b"
    4.27 +val x = Free ("x", xT)
    4.28 +val y = Free ("y", yT)
    4.29  val P  = mk_free "P" (xT-->yT-->propT)
    4.30  val Q  = mk_free "Q" (xT-->yT)
    4.31  val R  = mk_free "R" (xT-->yT)
    4.32 @@ -436,7 +440,7 @@
    4.33  fun quant_simproc thy = Simplifier.simproc_i
    4.34                             thy
    4.35                             "Ordered rewriting of nested quantifiers"
    4.36 -                           [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
    4.37 +                           [Logic.all x (Logic.all y (P $ x $ y))]
    4.38                             quant_rewrite
    4.39  fun eta_expand_simproc thy = Simplifier.simproc_i
    4.40                           thy
    4.41 @@ -446,7 +450,7 @@
    4.42  fun eta_contract_simproc thy = Simplifier.simproc_i
    4.43                           thy
    4.44                           "Smart handling of eta-contractions"
    4.45 -                         [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
    4.46 +                         [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
    4.47                           eta_contract
    4.48  end
    4.49  
    4.50 @@ -582,8 +586,7 @@
    4.51  fun set_prop thy t =
    4.52      let
    4.53          val vars = add_term_frees (t,add_term_vars (t,[]))
    4.54 -        val closed_t = Library.foldr (fn (v, body) =>
    4.55 -      let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
    4.56 +        val closed_t = fold_rev Logic.all vars t
    4.57          val rew_th = norm_term thy closed_t
    4.58          val rhs = Thm.rhs_of rew_th
    4.59  
     5.1 --- a/src/HOL/Statespace/state_fun.ML	Mon Jun 23 20:00:58 2008 +0200
     5.2 +++ b/src/HOL/Statespace/state_fun.ML	Mon Jun 23 23:45:39 2008 +0200
     5.3 @@ -251,7 +251,7 @@
     5.4                 (trm,trm',vars,_,true)
     5.5                  => let
     5.6                       val eq1 = Goal.prove ctxt [] [] 
     5.7 -                                      (list_all (vars,equals sT$trm$trm'))
     5.8 +                                      (list_all (vars, Logic.mk_equals (trm, trm')))
     5.9                                        (fn _ => rtac meta_ext 1 THEN 
    5.10                                                 simp_tac ss1 1);
    5.11                       val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
     6.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 23 20:00:58 2008 +0200
     6.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 23 23:45:39 2008 +0200
     6.3 @@ -637,8 +637,8 @@
     6.4    let
     6.5      val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
     6.6    in
     6.7 -    equals propT $ HOLogic.mk_Trueprop t $
     6.8 -      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
     6.9 +    Logic.mk_equals (HOLogic.mk_Trueprop t,
    6.10 +      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
    6.11    end;
    6.12  
    6.13  end;
     7.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jun 23 20:00:58 2008 +0200
     7.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jun 23 23:45:39 2008 +0200
     7.3 @@ -237,8 +237,8 @@
     7.4          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
     7.5          val lhs = list_comb (Const (cname, constrT), l_args);
     7.6          val rhs = mk_univ_inj r_args n i;
     7.7 -        val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
     7.8 -        val def_name = (Sign.base_name cname) ^ "_def";
     7.9 +        val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
    7.10 +        val def_name = Sign.base_name cname ^ "_def";
    7.11          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    7.12            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
    7.13          val ([def_thm], thy') =
    7.14 @@ -346,8 +346,8 @@
    7.15          val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
    7.16          val fTs = map fastype_of fs;
    7.17          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    7.18 -          equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
    7.19 -            list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
    7.20 +          Logic.mk_equals (Const (iso_name, T --> Univ_elT),
    7.21 +            list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
    7.22          val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
    7.23  
    7.24          (* prove characteristic equations *)
     8.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 23 20:00:58 2008 +0200
     8.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 23 23:45:39 2008 +0200
     8.3 @@ -177,7 +177,7 @@
     8.4  
     8.5  fun export_term (fixes, assumes) =
     8.6      fold_rev (curry Logic.mk_implies o prop_of) assumes 
     8.7 - #> fold_rev (mk_forall o Free) fixes
     8.8 + #> fold_rev (Logic.all o Free) fixes
     8.9  
    8.10  fun export_thm thy (fixes, assumes) =
    8.11      fold_rev (implies_intr o cprop_of) assumes
     9.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 23 20:00:58 2008 +0200
     9.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 23 23:45:39 2008 +0200
     9.3 @@ -152,7 +152,7 @@
     9.4          fun mk_assum qs pats = 
     9.5              HOLogic.mk_Trueprop P
     9.6              |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
     9.7 -            |> fold_rev mk_forall qs
     9.8 +            |> fold_rev Logic.all qs
     9.9              |> cterm_of thy
    9.10  
    9.11          val hyps = map2 mk_assum qss patss
    9.12 @@ -221,7 +221,7 @@
    9.13              HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    9.14                            Const ("HOL.undefined", rT))
    9.15                |> HOLogic.mk_Trueprop
    9.16 -              |> fold_rev mk_forall qs
    9.17 +              |> fold_rev Logic.all qs
    9.18            end
    9.19      in
    9.20        map mk_eqn fixes
    10.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 23 20:00:58 2008 +0200
    10.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 23 23:45:39 2008 +0200
    10.3 @@ -21,9 +21,6 @@
    10.4  fun plural sg pl [x] = sg
    10.5    | plural sg pl _ = pl
    10.6  
    10.7 -(* ==> logic.ML? *)
    10.8 -fun mk_forall v t = all (fastype_of v) $ lambda v t
    10.9 -
   10.10  (* lambda-abstracts over an arbitrarily nested tuple
   10.11    ==> hologic.ML? *)
   10.12  fun tupled_lambda vars t =
   10.13 @@ -117,7 +114,7 @@
   10.14    | rename_bound n _ = raise Match
   10.15  
   10.16  fun mk_forall_rename (n, v) =
   10.17 -    rename_bound n o mk_forall v 
   10.18 +    rename_bound n o Logic.all v 
   10.19  
   10.20  val dummy_term = Free ("", dummyT)
   10.21  
    11.1 --- a/src/HOL/Tools/function_package/induction_scheme.ML	Mon Jun 23 20:00:58 2008 +0200
    11.2 +++ b/src/HOL/Tools/function_package/induction_scheme.ML	Mon Jun 23 23:45:39 2008 +0200
    11.3 @@ -146,7 +146,7 @@
    11.4        HOLogic.mk_Trueprop Pbool
    11.5         |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
    11.6         |> fold_rev (curry Logic.mk_implies) Cs'
    11.7 -       |> fold_rev (mk_forall o Free) ws
    11.8 +       |> fold_rev (Logic.all o Free) ws
    11.9         |> fold_rev mk_forall_rename (map fst xs ~~ xs')
   11.10         |> mk_forall_rename ("P", Pbool)
   11.11      end
   11.12 @@ -169,7 +169,7 @@
   11.13              val cse = 
   11.14                  HOLogic.mk_Trueprop thesis
   11.15                  |> fold_rev (curry Logic.mk_implies) Cs'
   11.16 -                |> fold_rev (mk_forall o Free) ws
   11.17 +                |> fold_rev (Logic.all o Free) ws
   11.18            in
   11.19              Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
   11.20            end
   11.21 @@ -180,7 +180,7 @@
   11.22                  let val export = 
   11.23                           fold_rev (curry Logic.mk_implies) Gas
   11.24                           #> fold_rev (curry Logic.mk_implies) gs
   11.25 -                         #> fold_rev (mk_forall o Free) Gvs
   11.26 +                         #> fold_rev (Logic.all o Free) Gvs
   11.27                           #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   11.28                  in
   11.29                  (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
   11.30 @@ -188,7 +188,7 @@
   11.31                   |> export,
   11.32                   mk_pres bidx' rcarg
   11.33                   |> export
   11.34 -                 |> mk_forall thesis)
   11.35 +                 |> Logic.all thesis)
   11.36                  end
   11.37            in
   11.38              map g rs
   11.39 @@ -205,7 +205,7 @@
   11.40        fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   11.41            HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   11.42            |> fold_rev (curry Logic.mk_implies) Cs
   11.43 -          |> fold_rev (mk_forall o Free) ws
   11.44 +          |> fold_rev (Logic.all o Free) ws
   11.45            |> term_conv thy ind_atomize
   11.46            |> ObjectLogic.drop_judgment thy
   11.47            |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   11.48 @@ -230,13 +230,13 @@
   11.49        val P_comp = mk_ind_goal thy branches
   11.50  
   11.51        (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   11.52 -      val ihyp = all T $ Abs ("z", T, 
   11.53 -               implies $ 
   11.54 -                  HOLogic.mk_Trueprop (
   11.55 +      val ihyp = Term.all T $ Abs ("z", T, 
   11.56 +               Logic.mk_implies
   11.57 +                 (HOLogic.mk_Trueprop (
   11.58                    Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
   11.59                      $ (HOLogic.pair_const T T $ Bound 0 $ x) 
   11.60 -                    $ R)
   11.61 -             $ HOLogic.mk_Trueprop (P_comp $ Bound 0))
   11.62 +                    $ R),
   11.63 +                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
   11.64             |> cert
   11.65  
   11.66        val aihyp = assume ihyp
   11.67 @@ -290,7 +290,7 @@
   11.68                    val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
   11.69                               |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   11.70                               |> fold_rev (curry Logic.mk_implies) gs
   11.71 -                             |> fold_rev (mk_forall o Free) qs
   11.72 +                             |> fold_rev (Logic.all o Free) qs
   11.73                               |> cert
   11.74                               
   11.75                    val Plhs_to_Pxs_conv = 
    12.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Jun 23 20:00:58 2008 +0200
    12.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Jun 23 23:45:39 2008 +0200
    12.3 @@ -70,8 +70,7 @@
    12.4      let
    12.5        val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
    12.6      in
    12.7 -      Logic.list_implies (prems, concl)
    12.8 -        |> fold_rev FundefLib.mk_forall vars
    12.9 +      fold_rev Logic.all vars (Logic.list_implies (prems, concl))
   12.10      end
   12.11  
   12.12  fun prove thy solve_tac t =
    13.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Mon Jun 23 20:00:58 2008 +0200
    13.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Mon Jun 23 23:45:39 2008 +0200
    13.3 @@ -101,7 +101,7 @@
    13.4            let
    13.5              val t = Pattern.rewrite_term thy sigma [] feq1
    13.6            in
    13.7 -            fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
    13.8 +            fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
    13.9            end
   13.10      in
   13.11        map instantiate substs
    14.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Jun 23 20:00:58 2008 +0200
    14.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Jun 23 23:45:39 2008 +0200
    14.3 @@ -29,14 +29,10 @@
    14.4      val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    14.5    in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    14.6  
    14.7 -fun forall_intr_prf (t, prf) =
    14.8 +fun forall_intr_prf t prf =
    14.9    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   14.10    in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
   14.11  
   14.12 -fun forall_intr_term (t, u) =
   14.13 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   14.14 -  in all T $ Abs (a, T, abstract_over (t, u)) end;
   14.15 -
   14.16  fun subsets [] = [[]]
   14.17    | subsets (x::xs) =
   14.18        let val ys = subsets xs
   14.19 @@ -264,13 +260,13 @@
   14.20      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
   14.21      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
   14.22      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
   14.23 -    val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
   14.24 -    val rlz'' = foldr forall_intr_term rlz vs2
   14.25 +    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
   14.26 +    val rlz'' = fold_rev Logic.all vs2 rlz
   14.27    in (name, (vs,
   14.28      if rt = Extraction.nullt then rt else
   14.29        foldr (uncurry lambda) rt vs1,
   14.30      ProofRewriteRules.un_hhf_proof rlz' rlz''
   14.31 -      (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
   14.32 +      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
   14.33    end;
   14.34  
   14.35  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
   14.36 @@ -427,7 +423,7 @@
   14.37        let
   14.38          val (prem :: prems) = prems_of elim;
   14.39          fun reorder1 (p, (_, intr)) =
   14.40 -          Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
   14.41 +          Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
   14.42              (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
   14.43          fun reorder2 ((ivs, intr), i) =
   14.44            let val fs = Term.add_vars (prop_of intr) [] \\ params'
    15.1 --- a/src/HOL/Tools/inductive_set_package.ML	Mon Jun 23 20:00:58 2008 +0200
    15.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Mon Jun 23 23:45:39 2008 +0200
    15.3 @@ -69,7 +69,7 @@
    15.4        fun close p t f =
    15.5          let val vs = Term.add_vars t []
    15.6          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    15.7 -          (p (fold (fn x as (_, T) => fn u => all T $ lambda (Var x) u) vs t) f)
    15.8 +          (p (fold (Logic.all o Var) vs t) f)
    15.9          end;
   15.10        fun mkop "op &" T x = SOME (Const ("op Int", T --> T --> T), x)
   15.11          | mkop "op |" T x = SOME (Const ("op Un", T --> T --> T), x)
    16.1 --- a/src/HOL/Tools/record_package.ML	Mon Jun 23 20:00:58 2008 +0200
    16.2 +++ b/src/HOL/Tools/record_package.ML	Mon Jun 23 23:45:39 2008 +0200
    16.3 @@ -1050,7 +1050,7 @@
    16.4                (case mk_eq_terms (upd$k$r) of
    16.5                   SOME (trm,trm',vars)
    16.6                   => SOME (prove_split_simp thy ss domS
    16.7 -                                 (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
    16.8 +                                 (list_all(vars, Logic.mk_equals (sel $ trm, trm'))))
    16.9                 | NONE => NONE)
   16.10              end
   16.11            | NONE => NONE)
   16.12 @@ -1187,7 +1187,7 @@
   16.13                 Inter (trm,trm',vars,_,_)
   16.14                  => SOME (normalize_rhs 
   16.15                            (prove_split_simp thy ss rT
   16.16 -                            (list_all(vars,(equals rT$trm$trm')))))
   16.17 +                            (list_all(vars, Logic.mk_equals (trm, trm')))))
   16.18               | _ => NONE)
   16.19           end
   16.20         | _ => NONE))
    17.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Jun 23 20:00:58 2008 +0200
    17.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Jun 23 23:45:39 2008 +0200
    17.3 @@ -86,7 +86,7 @@
    17.4                      (*Forms a lambda-abstraction over the formal parameters*)
    17.5              val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
    17.6              val cdef = cname ^ "_def"
    17.7 -            val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
    17.8 +            val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
    17.9              val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
   17.10            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
   17.11        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
   17.12 @@ -113,7 +113,7 @@
   17.13                  val rhs = list_abs_free (map dest_Free args,
   17.14                                           HOLogic.choice_const T $ xtp)
   17.15                        (*Forms a lambda-abstraction over the formal parameters*)
   17.16 -                val def = equals cT $ c $ rhs
   17.17 +                val def = Logic.mk_equals (c, rhs)
   17.18              in dec_sko (subst_bound (list_comb(c,args), p))
   17.19                         (def :: defs)
   17.20              end
    18.1 --- a/src/HOL/Tools/res_reconstruct.ML	Mon Jun 23 20:00:58 2008 +0200
    18.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Mon Jun 23 23:45:39 2008 +0200
    18.3 @@ -250,12 +250,7 @@
    18.4      singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
    18.5    end;
    18.6  
    18.7 -(*Quantification over a list of Vars. FIXME: for term.ML??*)
    18.8 -fun list_all_var ([], t: term) = t
    18.9 -  | list_all_var ((v as Var(ix,T)) :: vars, t) =
   18.10 -      (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
   18.11 -
   18.12 -fun gen_all_vars t = list_all_var (term_vars t, t);
   18.13 +fun gen_all_vars t = fold_rev Logic.all (term_vars t) t;
   18.14  
   18.15  fun ints_of_stree_aux (Int n, ns) = n::ns
   18.16    | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
    19.1 --- a/src/Pure/Proof/extraction.ML	Mon Jun 23 20:00:58 2008 +0200
    19.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jun 23 23:45:39 2008 +0200
    19.3 @@ -128,10 +128,6 @@
    19.4  fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
    19.5  fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
    19.6  
    19.7 -fun forall_intr (t, prop) =
    19.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    19.9 -  in all T $ Abs (a, T, abstract_over (t, prop)) end;
   19.10 -
   19.11  fun forall_intr_prf (t, prf) =
   19.12    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   19.13    in Abst (a, SOME T, prf_abstract_over t prf) end;
   19.14 @@ -324,7 +320,7 @@
   19.15          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   19.16            (Const ("realizes", T --> propT --> propT) $
   19.17              (if T = nullT then t else list_comb (t, vars')) $ prop);
   19.18 -      val r = List.foldr forall_intr r' (map (get_var_type r') vars);
   19.19 +      val r = fold_rev Logic.all (map (get_var_type r') vars) r';
   19.20        val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
   19.21      in (name, (vs, (t, prf))) end
   19.22    end;
    20.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Jun 23 20:00:58 2008 +0200
    20.2 +++ b/src/Pure/Proof/reconstruct.ML	Mon Jun 23 23:45:39 2008 +0200
    20.3 @@ -26,11 +26,7 @@
    20.4  fun vars_of t = rev (fold_aterms
    20.5    (fn v as Var _ => insert (op =) v | _ => I) t []);
    20.6  
    20.7 -fun forall_intr t prop =
    20.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    20.9 -  in all T $ Abs (a, T, abstract_over (t, prop)) end;
   20.10 -
   20.11 -fun forall_intr_vfs prop = fold_rev forall_intr
   20.12 +fun forall_intr_vfs prop = fold_rev Logic.all
   20.13    (vars_of prop @ sort Term.term_ord (term_frees prop)) prop;
   20.14  
   20.15  fun forall_intr_prf t prf =
   20.16 @@ -317,7 +313,7 @@
   20.17  
   20.18  fun prop_of0 Hs (PBound i) = List.nth (Hs, i)
   20.19    | prop_of0 Hs (Abst (s, SOME T, prf)) =
   20.20 -      all T $ (Abs (s, T, prop_of0 Hs prf))
   20.21 +      Term.all T $ (Abs (s, T, prop_of0 Hs prf))
   20.22    | prop_of0 Hs (AbsP (s, SOME t, prf)) =
   20.23        Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
   20.24    | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
    21.1 --- a/src/Pure/proofterm.ML	Mon Jun 23 20:00:58 2008 +0200
    21.2 +++ b/src/Pure/proofterm.ML	Mon Jun 23 23:45:39 2008 +0200
    21.3 @@ -774,13 +774,10 @@
    21.4     ("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))),
    21.5     ("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))),
    21.6     ("equal_elim", list_implies ([mk_equals (A, B), A], B)),
    21.7 -   ("abstract_rule", Logic.mk_implies
    21.8 -      (all aT $ Abs ("x", aT, equals bT $ (f $ Bound 0) $ (g $ Bound 0)),
    21.9 -       equals (aT --> bT) $
   21.10 -         Abs ("x", aT, f $ Bound 0) $ Abs ("x", aT, g $ Bound 0))),
   21.11 -   ("combination", Logic.list_implies
   21.12 -      ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)],
   21.13 -       Logic.mk_equals (f $ x, g $ y)))];
   21.14 +   ("abstract_rule", mk_implies
   21.15 +      (all x (mk_equals (f $ x, g $ x)), mk_equals (lambda x (f $ x), lambda x (g $ x)))),
   21.16 +   ("combination", list_implies
   21.17 +      ([mk_equals (f, g), mk_equals (x, y)], mk_equals (f $ x, g $ y)))];
   21.18  
   21.19  val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
   21.20    equal_elim_axm, abstract_rule_axm, combination_axm] =