src/HOL/blastdata.ML
changeset 10906 de95ba2760fe
parent 10429 8820f787e61e
child 11753 02b257ef0ee2
--- a/src/HOL/blastdata.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/HOL/blastdata.ML	Tue Jan 16 00:28:50 2001 +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	= atomize_rules
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;