diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -97,9 +97,8 @@
 
 (** theory context references **)
 
-val inductive_forall_def = @{thm induct_forall_def};
-val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = @{thm induct_conj_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
+val inductive_conj_def = @{thm HOL.induct_conj_def};
 val inductive_conj = @{thms induct_conj};
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
@@ -689,7 +688,7 @@
                 val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
                 val Q =
                   fold_rev Term.abs (mk_names "x" k ~~ Ts)
-                    (HOLogic.mk_binop inductive_conj_name
+                    (HOLogic.mk_binop @{const_name HOL.induct_conj}
                       (list_comb (incr_boundvars k s, bs), P));
               in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
           | NONE =>