# HG changeset patch
# User wenzelm
# Date 965422645 -7200
# Node ID f0ffd29fd4e41cf363868e227c4ef144c5edc39f
# Parent  d9434a9277a4d6644a6faf9faecb6ac214d6aba6
val atomize = thms "atomize";

diff -r d9434a9277a4 -r f0ffd29fd4e4 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Fri Aug 04 22:56:52 2000 +0200
+++ b/src/HOL/blastdata.ML	Fri Aug 04 22:57:25 2000 +0200
@@ -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	= [thm "all_eq", thm "imp_eq"]
+  val atomize	= thms "atomize"
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;