discontinued old-style Term.list_all_free in favour of plain Logic.all;
authorwenzelm
Sat Jan 14 17:45:04 2012 +0100 (2012-01-14)
changeset 462150da9433f959e
parent 46214 8534f949548e
child 46216 7fcdb5562461
discontinued old-style Term.list_all_free in favour of plain Logic.all;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/record.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/specification.ML
src/Pure/logic.ML
src/Pure/term.ML
src/Tools/misc_legacy.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 16:58:29 2012 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 17:45:04 2012 +0100
     1.3 @@ -1155,9 +1155,11 @@
     1.4            mk_fresh1 [] (maps fst frees') @
     1.5            mk_fresh2 [] frees'
     1.6  
     1.7 -      in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
     1.8 -        HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
     1.9 -          list_comb (Const (cname, Ts ---> T), map Free frees))))
    1.10 +      in
    1.11 +        fold_rev (Logic.all o Free) (frees @ [z])
    1.12 +          (Logic.list_implies (prems' @ prems,
    1.13 +            HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
    1.14 +              list_comb (Const (cname, Ts ---> T), map Free frees))))
    1.15        end;
    1.16  
    1.17      val ind_prems = maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
    1.18 @@ -1173,8 +1175,8 @@
    1.19      val induct = Logic.list_implies (ind_prems, ind_concl);
    1.20  
    1.21      val ind_prems' =
    1.22 -      map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
    1.23 -        HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
    1.24 +      map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
    1.25 +        (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
    1.26            Term.range_type T -->
    1.27              HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
    1.28        maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
    1.29 @@ -1462,9 +1464,9 @@
    1.30          (rec_intr_ts @ [Logic.list_implies (flat prems2 @ prems3 @ prems1,
    1.31             HOLogic.mk_Trueprop (rec_set $
    1.32               list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
    1.33 -         rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
    1.34 -         rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
    1.35 -           Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
    1.36 +         rec_prems @ [fold_rev (Logic.all o Free) (frees @ frees'') (Logic.list_implies (prems4, P))],
    1.37 +         rec_prems' @ map (fn fr => fold_rev (Logic.all o Free) (frees @ frees'')
    1.38 +           (Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
    1.39               HOLogic.mk_Trueprop fr))) result_freshs,
    1.40           rec_eq_prems @ [flat prems2 @ prems3],
    1.41           l + 1)
     2.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Jan 14 16:58:29 2012 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Jan 14 17:45:04 2012 +0100
     2.3 @@ -332,7 +332,7 @@
     2.4      val cprems = map cert prems;
     2.5      val asms = map Thm.assume cprems;
     2.6      val premss = map (fn (cargs, eprems, eqn) =>
     2.7 -      map (fn t => list_all_free (cargs, Logic.list_implies (eprems, t)))
     2.8 +      map (fn t => fold_rev (Logic.all o Free) cargs (Logic.list_implies (eprems, t)))
     2.9          (List.drop (prems_of eqn, length prems))) rec_rewrites';
    2.10      val cpremss = map (map cert) premss;
    2.11      val asmss = map (map Thm.assume) cpremss;
    2.12 @@ -355,7 +355,7 @@
    2.13        (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
    2.14  
    2.15      val goals = map (fn ((cargs, _, _), eqn) =>
    2.16 -      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns');
    2.17 +      (fold_rev (Logic.all o Free) cargs eqn, [])) (rec_rewrites' ~~ eqns');
    2.18  
    2.19    in
    2.20      lthy' |>
     3.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 16:58:29 2012 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 17:45:04 2012 +0100
     3.3 @@ -139,8 +139,8 @@
     3.4          val frees = tnames ~~ Ts;
     3.5          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
     3.6        in
     3.7 -        list_all_free (frees,
     3.8 -          Logic.list_implies (prems,
     3.9 +        fold_rev (Logic.all o Free) frees
    3.10 +          (Logic.list_implies (prems,
    3.11              HOLogic.mk_Trueprop (make_pred k T $
    3.12                list_comb (Const (cname, Ts ---> T), map Free frees))))
    3.13        end;
    3.14 @@ -167,8 +167,8 @@
    3.15          val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
    3.16          val free_ts = map Free frees;
    3.17        in
    3.18 -        list_all_free (frees,
    3.19 -          Logic.mk_implies (HOLogic.mk_Trueprop
    3.20 +        fold_rev (Logic.all o Free) frees
    3.21 +          (Logic.mk_implies (HOLogic.mk_Trueprop
    3.22              (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
    3.23                HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
    3.24        end;
    3.25 @@ -388,11 +388,12 @@
    3.26              val tnames = Name.variant_list used (make_tnames Ts);
    3.27              val frees = map Free (tnames ~~ Ts);
    3.28            in
    3.29 -            list_all_free (tnames ~~ Ts, Logic.mk_implies
    3.30 -              (HOLogic.mk_Trueprop
    3.31 -                (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
    3.32 -               HOLogic.mk_Trueprop
    3.33 -                (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
    3.34 +            fold_rev Logic.all frees
    3.35 +              (Logic.mk_implies
    3.36 +                (HOLogic.mk_Trueprop
    3.37 +                  (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
    3.38 +                 HOLogic.mk_Trueprop
    3.39 +                  (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
    3.40            end;
    3.41        in
    3.42          Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::
     4.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 16:58:29 2012 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 17:45:04 2012 +0100
     4.3 @@ -42,7 +42,7 @@
     4.4        else Free (nth pnames i, U --> HOLogic.boolT) $ x;
     4.5  
     4.6      fun mk_all i s T t =
     4.7 -      if member (op =) is i then list_all_free ([(s, T)], t) else t;
     4.8 +      if member (op =) is i then Logic.all (Free (s, T)) t else t;
     4.9  
    4.10      val (prems, rec_fns) = split_list (flat (fst (fold_map
    4.11        (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    4.12 @@ -78,7 +78,7 @@
    4.13                        (make_pred k rT U (Datatype_Aux.app_bnds r i)
    4.14                          (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
    4.15                  end;
    4.16 -        in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
    4.17 +        in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
    4.18            constrs) (descr ~~ recTs) 1)));
    4.19  
    4.20      fun mk_proj j [] t = t
    4.21 @@ -170,10 +170,11 @@
    4.22          val free_ts = map Free frees;
    4.23          val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
    4.24        in
    4.25 -        (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
    4.26 -          (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
    4.27 -            HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
    4.28 -              list_comb (r, free_ts)))))
    4.29 +        (r, fold_rev Logic.all free_ts
    4.30 +          (Logic.mk_implies (HOLogic.mk_Trueprop
    4.31 +            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
    4.32 +              HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
    4.33 +                list_comb (r, free_ts)))))
    4.34        end;
    4.35  
    4.36      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
     5.1 --- a/src/HOL/Tools/inductive.ML	Sat Jan 14 16:58:29 2012 +0100
     5.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 17:45:04 2012 +0100
     5.3 @@ -309,7 +309,7 @@
     5.4      val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
     5.5      val rule' = Logic.list_implies (prems, concl);
     5.6      val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
     5.7 -    val arule = list_all_free (params', Logic.list_implies (aprems, concl));
     5.8 +    val arule = fold_rev (Logic.all o Free) params' (Logic.list_implies (aprems, concl));
     5.9  
    5.10      fun check_ind err t =
    5.11        (case dest_predicate cs params t of
    5.12 @@ -670,8 +670,8 @@
    5.13          val SOME (_, i, ys, _) =
    5.14            dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
    5.15        in
    5.16 -        list_all_free (Logic.strip_params r,
    5.17 -          Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    5.18 +        fold_rev (Logic.all o Free) (Logic.strip_params r)
    5.19 +          (Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    5.20              (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
    5.21                HOLogic.mk_Trueprop (list_comb (nth preds i, ys))))
    5.22        end;
    5.23 @@ -1016,11 +1016,12 @@
    5.24      val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
    5.25      val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;
    5.26  
    5.27 -    fun close_rule r = list_all_free (rev (fold_aterms
    5.28 -      (fn t as Free (v as (s, _)) =>
    5.29 -          if Variable.is_fixed ctxt1 s orelse
    5.30 -            member (op =) ps t then I else insert (op =) v
    5.31 -        | _ => I) r []), r);
    5.32 +    fun close_rule r =
    5.33 +      fold (Logic.all o Free) (fold_aterms
    5.34 +        (fn t as Free (v as (s, _)) =>
    5.35 +            if Variable.is_fixed ctxt1 s orelse
    5.36 +              member (op =) ps t then I else insert (op =) v
    5.37 +          | _ => I) r []) r;
    5.38  
    5.39      val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
    5.40      val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';
     6.1 --- a/src/HOL/Tools/record.ML	Sat Jan 14 16:58:29 2012 +0100
     6.2 +++ b/src/HOL/Tools/record.ML	Sat Jan 14 17:45:04 2012 +0100
     6.3 @@ -243,7 +243,6 @@
     6.4  (* syntax *)
     6.5  
     6.6  val Trueprop = HOLogic.mk_Trueprop;
     6.7 -fun All xs t = Term.list_all_free (xs, t);
     6.8  
     6.9  infix 0 :== ===;
    6.10  infixr 0 ==>;
    6.11 @@ -1585,14 +1584,11 @@
    6.12            (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
    6.13        end;
    6.14  
    6.15 -    val induct_prop =
    6.16 -      (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
    6.17 +    val induct_prop = (fold_rev Logic.all vars_more (Trueprop (P $ ext)), Trueprop (P $ s));
    6.18  
    6.19      val split_meta_prop =  (* FIXME local P *)
    6.20 -      let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT) in
    6.21 -        Logic.mk_equals
    6.22 -         (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
    6.23 -      end;
    6.24 +      let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT)
    6.25 +      in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
    6.26  
    6.27      val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
    6.28        simplify HOL_ss
    6.29 @@ -2044,10 +2040,9 @@
    6.30  
    6.31      (*induct*)
    6.32      val induct_scheme_prop =
    6.33 -      All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
    6.34 +      fold_rev Logic.all all_vars_more (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
    6.35      val induct_prop =
    6.36 -      (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
    6.37 -        Trueprop (P_unit $ r_unit0));
    6.38 +      (fold_rev Logic.all all_vars (Trueprop (P_unit $ r_rec_unit0)), Trueprop (P_unit $ r_unit0));
    6.39  
    6.40      (*surjective*)
    6.41      val surjective_prop =
    6.42 @@ -2056,19 +2051,17 @@
    6.43  
    6.44      (*cases*)
    6.45      val cases_scheme_prop =
    6.46 -      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
    6.47 +      (fold_rev Logic.all all_vars_more ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
    6.48  
    6.49      val cases_prop =
    6.50 -      (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
    6.51 -         ==> Trueprop C;
    6.52 +      fold_rev Logic.all all_vars ((r_unit0 === r_rec_unit0) ==> Trueprop C) ==> Trueprop C;
    6.53  
    6.54      (*split*)
    6.55      val split_meta_prop =
    6.56        let
    6.57          val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT);
    6.58        in
    6.59 -        Logic.mk_equals
    6.60 -         (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
    6.61 +        Logic.mk_equals (Logic.all r0 (P $ r0), fold_rev Logic.all all_vars_more (P $ r_rec0))
    6.62        end;
    6.63  
    6.64      val split_object_prop =
    6.65 @@ -2085,7 +2078,7 @@
    6.66          val s' = Free (rN ^ "'", rec_schemeT0);
    6.67          fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
    6.68          val seleqs = map mk_sel_eq all_named_vars_more;
    6.69 -      in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
    6.70 +      in Logic.all r0 (Logic.all s' (Logic.list_implies (seleqs, r0 === s'))) end;
    6.71  
    6.72  
    6.73      (* 3rd stage: thms_thy *)
     7.1 --- a/src/Pure/Isar/obtain.ML	Sat Jan 14 16:58:29 2012 +0100
     7.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jan 14 17:45:04 2012 +0100
     7.3 @@ -130,7 +130,7 @@
     7.4  
     7.5      (*obtain parms*)
     7.6      val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
     7.7 -    val parms = xs' ~~ Ts;
     7.8 +    val parms = map Free (xs' ~~ Ts);
     7.9      val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
    7.10  
    7.11      (*obtain statements*)
    7.12 @@ -140,16 +140,16 @@
    7.13      val that_name = if name = "" then thatN else name;
    7.14      val that_prop =
    7.15        Logic.list_rename_params xs
    7.16 -        (Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)));
    7.17 +        (fold_rev Logic.all parms (Logic.list_implies (asm_props, thesis)));
    7.18      val obtain_prop =
    7.19        Logic.list_rename_params [Auto_Bind.thesisN]
    7.20 -        (Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
    7.21 +        (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
    7.22  
    7.23      fun after_qed _ =
    7.24        Proof.local_qed (NONE, false)
    7.25        #> `Proof.the_fact #-> (fn rule =>
    7.26          Proof.fix vars
    7.27 -        #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
    7.28 +        #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms);
    7.29    in
    7.30      state
    7.31      |> Proof.enter_forward
     8.1 --- a/src/Pure/Isar/specification.ML	Sat Jan 14 16:58:29 2012 +0100
     8.2 +++ b/src/Pure/Isar/specification.ML	Sat Jan 14 17:45:04 2012 +0100
     8.3 @@ -345,7 +345,8 @@
     8.4              val (Ts, _) = ctxt'
     8.5                |> fold Variable.declare_term props
     8.6                |> fold_map Proof_Context.inferred_param xs;
     8.7 -            val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
     8.8 +            val params = map Free (xs ~~ Ts);
     8.9 +            val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
    8.10              val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
    8.11            in
    8.12              ctxt'
     9.1 --- a/src/Pure/logic.ML	Sat Jan 14 16:58:29 2012 +0100
     9.2 +++ b/src/Pure/logic.ML	Sat Jan 14 17:45:04 2012 +0100
     9.3 @@ -337,8 +337,7 @@
     9.4  fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
     9.5  
     9.6  (*Close up a formula over all free variables by quantification*)
     9.7 -fun close_form A =
     9.8 -  Term.list_all_free (rev (Term.add_frees A []), A);
     9.9 +fun close_form A = fold (all o Free) (Term.add_frees A []) A;
    9.10  
    9.11  
    9.12  
    10.1 --- a/src/Pure/term.ML	Sat Jan 14 16:58:29 2012 +0100
    10.2 +++ b/src/Pure/term.ML	Sat Jan 14 17:45:04 2012 +0100
    10.3 @@ -97,7 +97,6 @@
    10.4    val lambda: term -> term -> term
    10.5    val absfree: string * typ -> term -> term
    10.6    val absdummy: typ -> term -> term
    10.7 -  val list_all_free: (string * typ) list * term -> term
    10.8    val list_all: (string * typ) list * term -> term
    10.9    val subst_atomic: (term * term) list -> term -> term
   10.10    val typ_subst_atomic: (typ * typ) list -> typ -> typ
   10.11 @@ -764,11 +763,6 @@
   10.12  fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
   10.13  fun absdummy T body = Abs (Name.uu_, T, body);
   10.14  
   10.15 -(*Quantification over a list of free variables*)
   10.16 -fun list_all_free ([], t: term) = t
   10.17 -  | list_all_free ((a,T)::vars, t) =
   10.18 -        all T $ absfree (a, T) (list_all_free (vars, t));
   10.19 -
   10.20  (*Quantification over a list of variables (already bound in body) *)
   10.21  fun list_all ([], t) = t
   10.22    | list_all ((a,T)::vars, t) =
    11.1 --- a/src/Tools/misc_legacy.ML	Sat Jan 14 16:58:29 2012 +0100
    11.2 +++ b/src/Tools/misc_legacy.ML	Sat Jan 14 17:45:04 2012 +0100
    11.3 @@ -180,7 +180,7 @@
    11.4            if in_concl then (cterm u, cterm (Var ((a, i), T)))
    11.5            else (cterm u, cterm (Var ((a, i + maxidx), U)))
    11.6        (*Embed B in the original context of params and hyps*)
    11.7 -      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
    11.8 +      fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
    11.9        (*Strip the context using elimination rules*)
   11.10        fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   11.11        (*A form of lifting that discharges assumptions.*)
    12.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Jan 14 16:58:29 2012 +0100
    12.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 14 17:45:04 2012 +0100
    12.3 @@ -296,13 +296,13 @@
    12.4  
    12.5       (*Make a premise of the induction rule.*)
    12.6       fun induct_prem ind_alist intr =
    12.7 -       let val quantfrees = map dest_Free (subtract (op =) rec_params (Misc_Legacy.term_frees intr))
    12.8 +       let val xs = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
    12.9             val iprems = List.foldr (add_induct_prem ind_alist) []
   12.10                                (Logic.strip_imp_prems intr)
   12.11             val (t,X) = Ind_Syntax.rule_concl intr
   12.12             val (SOME pred) = AList.lookup (op aconv) ind_alist X
   12.13             val concl = FOLogic.mk_Trueprop (pred $ t)
   12.14 -       in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
   12.15 +       in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end
   12.16         handle Bind => error"Recursion term not found in conclusion";
   12.17  
   12.18       (*Minimizes backtracking by delivering the correct premise to each goal.