src/HOL/Tools/inductive.ML
changeset 46215 0da9433f959e
parent 45740 132a3e1c0fe5
child 46218 ecf6375e2abb
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Jan 14 16:58:29 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 17:45:04 2012 +0100
     1.3 @@ -309,7 +309,7 @@
     1.4      val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
     1.5      val rule' = Logic.list_implies (prems, concl);
     1.6      val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
     1.7 -    val arule = list_all_free (params', Logic.list_implies (aprems, concl));
     1.8 +    val arule = fold_rev (Logic.all o Free) params' (Logic.list_implies (aprems, concl));
     1.9  
    1.10      fun check_ind err t =
    1.11        (case dest_predicate cs params t of
    1.12 @@ -670,8 +670,8 @@
    1.13          val SOME (_, i, ys, _) =
    1.14            dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
    1.15        in
    1.16 -        list_all_free (Logic.strip_params r,
    1.17 -          Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    1.18 +        fold_rev (Logic.all o Free) (Logic.strip_params r)
    1.19 +          (Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    1.20              (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
    1.21                HOLogic.mk_Trueprop (list_comb (nth preds i, ys))))
    1.22        end;
    1.23 @@ -1016,11 +1016,12 @@
    1.24      val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
    1.25      val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;
    1.26  
    1.27 -    fun close_rule r = list_all_free (rev (fold_aterms
    1.28 -      (fn t as Free (v as (s, _)) =>
    1.29 -          if Variable.is_fixed ctxt1 s orelse
    1.30 -            member (op =) ps t then I else insert (op =) v
    1.31 -        | _ => I) r []), r);
    1.32 +    fun close_rule r =
    1.33 +      fold (Logic.all o Free) (fold_aterms
    1.34 +        (fn t as Free (v as (s, _)) =>
    1.35 +            if Variable.is_fixed ctxt1 s orelse
    1.36 +              member (op =) ps t then I else insert (op =) v
    1.37 +          | _ => I) r []) r;
    1.38  
    1.39      val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
    1.40      val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';