diff -r 8941d8d15dc8 -r 02b257ef0ee2 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/Set.ML	Sun Oct 14 20:02:59 2001 +0200
@@ -844,12 +844,12 @@
 (* rulify setup *)
 
 Goal "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)";
-by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
-qed "ball_eq";
+by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
+qed "atomize_ball";
 
 local
   val ss = HOL_basic_ss addsimps
-    (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
+    [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
 in
 
 structure Rulify = RulifyFun