src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Sun Oct 14 19:59:15 2001 +0200
+++ b/src/FOL/simpdata.ML	Sun Oct 14 19:59:55 2001 +0200
@@ -369,7 +369,8 @@
 (* rulify setup *)
 
 local
-  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
+  val ss = FOL_basic_ss addsimps
+    [Drule.norm_hhf_eq, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
 in
 
 structure Rulify = RulifyFun