--- a/src/HOL/Tools/inductive_package.ML Thu Oct 18 21:03:43 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Oct 18 21:05:35 2001 +0200
@@ -73,10 +73,10 @@
val vimage_name = "Inverse_Image.vimage";
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
-val inductive_forall_name = "Inductive.forall";
-val inductive_forall_def = thm "forall_def";
-val inductive_conj_name = "Inductive.conj";
-val inductive_conj_def = thm "conj_def";
+val inductive_forall_name = "HOL.inductive_forall";
+val inductive_forall_def = thm "inductive_forall_def";
+val inductive_conj_name = "HOL.inductive_conj";
+val inductive_conj_def = thm "inductive_conj_def";
val inductive_conj = thms "inductive_conj";
val inductive_atomize = thms "inductive_atomize";
val inductive_rulify1 = thms "inductive_rulify1";