# HG changeset patch
# User wenzelm
# Date 1326559504 -3600
# Node ID 0da9433f959e7c98eab6be3c2f5f54a45e5917fc
# Parent  8534f949548e3fb61796eb3430813329a0f2b3fa
discontinued old-style Term.list_all_free in favour of plain Logic.all;

diff -r 8534f949548e -r 0da9433f959e src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -1155,9 +1155,11 @@
           mk_fresh1 [] (maps fst frees') @
           mk_fresh2 [] frees'
 
-      in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
-        HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
-          list_comb (Const (cname, Ts ---> T), map Free frees))))
+      in
+        fold_rev (Logic.all o Free) (frees @ [z])
+          (Logic.list_implies (prems' @ prems,
+            HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
+              list_comb (Const (cname, Ts ---> T), map Free frees))))
       end;
 
     val ind_prems = maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
@@ -1173,8 +1175,8 @@
     val induct = Logic.list_implies (ind_prems, ind_concl);
 
     val ind_prems' =
-      map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
-        HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
+      map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
+        (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
           Term.range_type T -->
             HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
       maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
@@ -1462,9 +1464,9 @@
         (rec_intr_ts @ [Logic.list_implies (flat prems2 @ prems3 @ prems1,
            HOLogic.mk_Trueprop (rec_set $
              list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
-         rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
-         rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
-           Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
+         rec_prems @ [fold_rev (Logic.all o Free) (frees @ frees'') (Logic.list_implies (prems4, P))],
+         rec_prems' @ map (fn fr => fold_rev (Logic.all o Free) (frees @ frees'')
+           (Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
              HOLogic.mk_Trueprop fr))) result_freshs,
          rec_eq_prems @ [flat prems2 @ prems3],
          l + 1)
diff -r 8534f949548e -r 0da9433f959e src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -332,7 +332,7 @@
     val cprems = map cert prems;
     val asms = map Thm.assume cprems;
     val premss = map (fn (cargs, eprems, eqn) =>
-      map (fn t => list_all_free (cargs, Logic.list_implies (eprems, t)))
+      map (fn t => fold_rev (Logic.all o Free) cargs (Logic.list_implies (eprems, t)))
         (List.drop (prems_of eqn, length prems))) rec_rewrites';
     val cpremss = map (map cert) premss;
     val asmss = map (map Thm.assume) cpremss;
@@ -355,7 +355,7 @@
       (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
 
     val goals = map (fn ((cargs, _, _), eqn) =>
-      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns');
+      (fold_rev (Logic.all o Free) cargs eqn, [])) (rec_rewrites' ~~ eqns');
 
   in
     lthy' |>
diff -r 8534f949548e -r 0da9433f959e src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -139,8 +139,8 @@
         val frees = tnames ~~ Ts;
         val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
       in
-        list_all_free (frees,
-          Logic.list_implies (prems,
+        fold_rev (Logic.all o Free) frees
+          (Logic.list_implies (prems,
             HOLogic.mk_Trueprop (make_pred k T $
               list_comb (Const (cname, Ts ---> T), map Free frees))))
       end;
@@ -167,8 +167,8 @@
         val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
       in
-        list_all_free (frees,
-          Logic.mk_implies (HOLogic.mk_Trueprop
+        fold_rev (Logic.all o Free) frees
+          (Logic.mk_implies (HOLogic.mk_Trueprop
             (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
               HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
       end;
@@ -388,11 +388,12 @@
             val tnames = Name.variant_list used (make_tnames Ts);
             val frees = map Free (tnames ~~ Ts);
           in
-            list_all_free (tnames ~~ Ts, Logic.mk_implies
-              (HOLogic.mk_Trueprop
-                (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
-               HOLogic.mk_Trueprop
-                (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
+            fold_rev Logic.all frees
+              (Logic.mk_implies
+                (HOLogic.mk_Trueprop
+                  (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
+                 HOLogic.mk_Trueprop
+                  (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
           end;
       in
         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::
diff -r 8534f949548e -r 0da9433f959e src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -42,7 +42,7 @@
       else Free (nth pnames i, U --> HOLogic.boolT) $ x;
 
     fun mk_all i s T t =
-      if member (op =) is i then list_all_free ([(s, T)], t) else t;
+      if member (op =) is i then Logic.all (Free (s, T)) t else t;
 
     val (prems, rec_fns) = split_list (flat (fst (fold_map
       (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
@@ -78,7 +78,7 @@
                       (make_pred k rT U (Datatype_Aux.app_bnds r i)
                         (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
                 end;
-        in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
+        in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
           constrs) (descr ~~ recTs) 1)));
 
     fun mk_proj j [] t = t
@@ -170,10 +170,11 @@
         val free_ts = map Free frees;
         val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
       in
-        (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
-          (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
-            HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
-              list_comb (r, free_ts)))))
+        (r, fold_rev Logic.all free_ts
+          (Logic.mk_implies (HOLogic.mk_Trueprop
+            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
+              HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
+                list_comb (r, free_ts)))))
       end;
 
     val SOME (_, _, constrs) = AList.lookup (op =) descr index;
diff -r 8534f949548e -r 0da9433f959e src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -309,7 +309,7 @@
     val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
     val rule' = Logic.list_implies (prems, concl);
     val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
-    val arule = list_all_free (params', Logic.list_implies (aprems, concl));
+    val arule = fold_rev (Logic.all o Free) params' (Logic.list_implies (aprems, concl));
 
     fun check_ind err t =
       (case dest_predicate cs params t of
@@ -670,8 +670,8 @@
         val SOME (_, i, ys, _) =
           dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
       in
-        list_all_free (Logic.strip_params r,
-          Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
+        fold_rev (Logic.all o Free) (Logic.strip_params r)
+          (Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
             (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
               HOLogic.mk_Trueprop (list_comb (nth preds i, ys))))
       end;
@@ -1016,11 +1016,12 @@
     val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
     val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;
 
-    fun close_rule r = list_all_free (rev (fold_aterms
-      (fn t as Free (v as (s, _)) =>
-          if Variable.is_fixed ctxt1 s orelse
-            member (op =) ps t then I else insert (op =) v
-        | _ => I) r []), r);
+    fun close_rule r =
+      fold (Logic.all o Free) (fold_aterms
+        (fn t as Free (v as (s, _)) =>
+            if Variable.is_fixed ctxt1 s orelse
+              member (op =) ps t then I else insert (op =) v
+          | _ => I) r []) r;
 
     val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
     val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';
diff -r 8534f949548e -r 0da9433f959e src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Tools/record.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -243,7 +243,6 @@
 (* syntax *)
 
 val Trueprop = HOLogic.mk_Trueprop;
-fun All xs t = Term.list_all_free (xs, t);
 
 infix 0 :== ===;
 infixr 0 ==>;
@@ -1585,14 +1584,11 @@
           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
       end;
 
-    val induct_prop =
-      (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
+    val induct_prop = (fold_rev Logic.all vars_more (Trueprop (P $ ext)), Trueprop (P $ s));
 
     val split_meta_prop =  (* FIXME local P *)
-      let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT) in
-        Logic.mk_equals
-         (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
-      end;
+      let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT)
+      in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
 
     val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
       simplify HOL_ss
@@ -2044,10 +2040,9 @@
 
     (*induct*)
     val induct_scheme_prop =
-      All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
+      fold_rev Logic.all all_vars_more (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
     val induct_prop =
-      (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
-        Trueprop (P_unit $ r_unit0));
+      (fold_rev Logic.all all_vars (Trueprop (P_unit $ r_rec_unit0)), Trueprop (P_unit $ r_unit0));
 
     (*surjective*)
     val surjective_prop =
@@ -2056,19 +2051,17 @@
 
     (*cases*)
     val cases_scheme_prop =
-      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
+      (fold_rev Logic.all all_vars_more ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
 
     val cases_prop =
-      (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
-         ==> Trueprop C;
+      fold_rev Logic.all all_vars ((r_unit0 === r_rec_unit0) ==> Trueprop C) ==> Trueprop C;
 
     (*split*)
     val split_meta_prop =
       let
         val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT);
       in
-        Logic.mk_equals
-         (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
+        Logic.mk_equals (Logic.all r0 (P $ r0), fold_rev Logic.all all_vars_more (P $ r_rec0))
       end;
 
     val split_object_prop =
@@ -2085,7 +2078,7 @@
         val s' = Free (rN ^ "'", rec_schemeT0);
         fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
         val seleqs = map mk_sel_eq all_named_vars_more;
-      in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
+      in Logic.all r0 (Logic.all s' (Logic.list_implies (seleqs, r0 === s'))) end;
 
 
     (* 3rd stage: thms_thy *)
diff -r 8534f949548e -r 0da9433f959e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -130,7 +130,7 @@
 
     (*obtain parms*)
     val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
-    val parms = xs' ~~ Ts;
+    val parms = map Free (xs' ~~ Ts);
     val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
 
     (*obtain statements*)
@@ -140,16 +140,16 @@
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Logic.list_rename_params xs
-        (Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)));
+        (fold_rev Logic.all parms (Logic.list_implies (asm_props, thesis)));
     val obtain_prop =
       Logic.list_rename_params [Auto_Bind.thesisN]
-        (Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
+        (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
 
     fun after_qed _ =
       Proof.local_qed (NONE, false)
       #> `Proof.the_fact #-> (fn rule =>
         Proof.fix vars
-        #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
+        #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms);
   in
     state
     |> Proof.enter_forward
diff -r 8534f949548e -r 0da9433f959e src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -345,7 +345,8 @@
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props
               |> fold_map Proof_Context.inferred_param xs;
-            val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
+            val params = map Free (xs ~~ Ts);
+            val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
             val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
           in
             ctxt'
diff -r 8534f949548e -r 0da9433f959e src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/Pure/logic.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -337,8 +337,7 @@
 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
 
 (*Close up a formula over all free variables by quantification*)
-fun close_form A =
-  Term.list_all_free (rev (Term.add_frees A []), A);
+fun close_form A = fold (all o Free) (Term.add_frees A []) A;
 
 
 
diff -r 8534f949548e -r 0da9433f959e src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/Pure/term.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -97,7 +97,6 @@
   val lambda: term -> term -> term
   val absfree: string * typ -> term -> term
   val absdummy: typ -> term -> term
-  val list_all_free: (string * typ) list * term -> term
   val list_all: (string * typ) list * term -> term
   val subst_atomic: (term * term) list -> term -> term
   val typ_subst_atomic: (typ * typ) list -> typ -> typ
@@ -764,11 +763,6 @@
 fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
 fun absdummy T body = Abs (Name.uu_, T, body);
 
-(*Quantification over a list of free variables*)
-fun list_all_free ([], t: term) = t
-  | list_all_free ((a,T)::vars, t) =
-        all T $ absfree (a, T) (list_all_free (vars, t));
-
 (*Quantification over a list of variables (already bound in body) *)
 fun list_all ([], t) = t
   | list_all ((a,T)::vars, t) =
diff -r 8534f949548e -r 0da9433f959e src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/Tools/misc_legacy.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -180,7 +180,7 @@
           if in_concl then (cterm u, cterm (Var ((a, i), T)))
           else (cterm u, cterm (Var ((a, i + maxidx), U)))
       (*Embed B in the original context of params and hyps*)
-      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
+      fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
       (*Strip the context using elimination rules*)
       fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
       (*A form of lifting that discharges assumptions.*)
diff -r 8534f949548e -r 0da9433f959e src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -296,13 +296,13 @@
 
      (*Make a premise of the induction rule.*)
      fun induct_prem ind_alist intr =
-       let val quantfrees = map dest_Free (subtract (op =) rec_params (Misc_Legacy.term_frees intr))
+       let val xs = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
            val iprems = List.foldr (add_induct_prem ind_alist) []
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr
            val (SOME pred) = AList.lookup (op aconv) ind_alist X
            val concl = FOLogic.mk_Trueprop (pred $ t)
-       in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
+       in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end
        handle Bind => error"Recursion term not found in conclusion";
 
      (*Minimizes backtracking by delivering the correct premise to each goal.