# HG changeset patch
# User wenzelm
# Date 965846583 -7200
# Node ID 714ad541a1338a50b94d869d8567b7efeef95791
# Parent  b87a6afe5881a0e745a757872457a65926e1fc8b
thms "atomize";

diff -r b87a6afe5881 -r 714ad541a133 src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Wed Aug 09 17:10:41 2000 +0200
+++ b/src/FOL/blastdata.ML	Wed Aug 09 20:43:03 2000 +0200
@@ -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	= [thm "all_eq", thm "imp_eq"]
+  val atomize	= thms "atomize"
   val cla_modifiers = Cla.cla_modifiers;
   val cla_meth' = Cla.cla_meth'
   end;