# HG changeset patch
# User wenzelm
# Date 1003431935 -7200
# Node ID d2421e124fa3007d01b7f389aed4464621aa3994
# Parent  84dc8a2479d4092374ce79e50156ac4b86d5a07b
moved atomize stuff to theory HOL;

diff -r 84dc8a2479d4 -r d2421e124fa3 src/HOL/Tools/inductive_package.ML
--- 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";