src/HOL/Tools/inductive.ML
changeset 59940 087d81f5213e
parent 59936 b8ffc3dc9e24
child 60097 d20ca79d50e4
     1.1 --- a/src/HOL/Tools/inductive.ML	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -97,9 +97,8 @@
     1.4  
     1.5  (** theory context references **)
     1.6  
     1.7 -val inductive_forall_def = @{thm induct_forall_def};
     1.8 -val inductive_conj_name = "HOL.induct_conj";
     1.9 -val inductive_conj_def = @{thm induct_conj_def};
    1.10 +val inductive_forall_def = @{thm HOL.induct_forall_def};
    1.11 +val inductive_conj_def = @{thm HOL.induct_conj_def};
    1.12  val inductive_conj = @{thms induct_conj};
    1.13  val inductive_atomize = @{thms induct_atomize};
    1.14  val inductive_rulify = @{thms induct_rulify};
    1.15 @@ -689,7 +688,7 @@
    1.16                  val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
    1.17                  val Q =
    1.18                    fold_rev Term.abs (mk_names "x" k ~~ Ts)
    1.19 -                    (HOLogic.mk_binop inductive_conj_name
    1.20 +                    (HOLogic.mk_binop @{const_name HOL.induct_conj}
    1.21                        (list_comb (incr_boundvars k s, bs), P));
    1.22                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
    1.23            | NONE =>