src/HOL/blastdata.ML

--- a/src/HOL/blastdata.ML	Tue Aug 01 11:55:27 2000 +0200
+++ b/src/HOL/blastdata.ML	Tue Aug 01 11:57:09 2000 +0200
@@ -23,6 +23,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
+  val atomize	= [thm "all_eq", thm "imp_eq"]
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;