src/HOL/Tools/inductive.ML
changeset 46219 426ed18eba43
parent 46218 ecf6375e2abb
child 46708 b138dee7bed3
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -652,9 +652,10 @@
     1.4                  val k = length Ts;
     1.5                  val bs = map Bound (k - 1 downto 0);
     1.6                  val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
     1.7 -                val Q = list_abs (mk_names "x" k ~~ Ts,
     1.8 -                  HOLogic.mk_binop inductive_conj_name
     1.9 -                    (list_comb (incr_boundvars k s, bs), P));
    1.10 +                val Q =
    1.11 +                  fold_rev Term.abs (mk_names "x" k ~~ Ts)
    1.12 +                    (HOLogic.mk_binop inductive_conj_name
    1.13 +                      (list_comb (incr_boundvars k s, bs), P));
    1.14                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
    1.15            | NONE =>
    1.16                (case s of
    1.17 @@ -760,9 +761,10 @@
    1.18              val l = length Us;
    1.19              val zs = map Bound (l - 1 downto 0);
    1.20            in
    1.21 -            list_abs (map (pair "z") Us, list_comb (p,
    1.22 -              make_bool_args' bs i @ make_args argTs
    1.23 -                ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
    1.24 +            fold_rev (Term.abs o pair "z") Us
    1.25 +              (list_comb (p,
    1.26 +                make_bool_args' bs i @ make_args argTs
    1.27 +                  ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
    1.28            end
    1.29        | NONE =>
    1.30            (case t of