# HG changeset patch
# User wenzelm
# Date 973879222 -3600
# Node ID 8820f787e61ef0534f5c6d8c4720fe4b336a910e
# Parent  8f15fbce549f04a6c416e564d159726103c60669
val atomize = thms "atomize'";

diff -r 8f15fbce549f -r 8820f787e61e src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/FOL/blastdata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -10,7 +10,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Cla.claset
   val rep_cs    = Cla.rep_cs
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   val cla_modifiers = Cla.cla_modifiers;
   val cla_meth' = Cla.cla_meth'
   end;
diff -r 8f15fbce549f -r 8820f787e61e src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/FOL/cladata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -24,7 +24,7 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
diff -r 8f15fbce549f -r 8820f787e61e src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/HOL/blastdata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -23,7 +23,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;
diff -r 8f15fbce549f -r 8820f787e61e src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/HOL/cladata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -47,7 +47,7 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   end;
 
 structure Classical = ClassicalFun(Classical_Data);