# HG changeset patch
# User wenzelm
# Date 1003082579 -7200
# Node ID 02b257ef0ee26e6aab99de139fdb48f560c76ae8
# Parent  8941d8d15dc82f19d61e25955486c0d841005a0c
improved atomize setup;

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
diff -r 8941d8d15dc8 -r 02b257ef0ee2 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/arith_data.ML	Sun Oct 14 20:02:59 2001 +0200
@@ -422,7 +422,7 @@
 
 in
 
-val arith_tac = fast_arith_tac ORELSE' (atomize_tac THEN' raw_arith_tac);
+val arith_tac = fast_arith_tac ORELSE' (ObjectLogic.atomize_tac THEN' raw_arith_tac);
 
 fun arith_method prems =
   Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
diff -r 8941d8d15dc8 -r 02b257ef0ee2 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/blastdata.ML	Sun Oct 14 20:02:59 2001 +0200
@@ -23,7 +23,6 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
-  val atomize	= atomize_rules
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;
diff -r 8941d8d15dc8 -r 02b257ef0ee2 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/cladata.ML	Sun Oct 14 20:02:59 2001 +0200
@@ -38,10 +38,6 @@
   compatibliity with strange things done in many existing proofs *)
 val cla_make_elim = Make_Elim.make_elim;
 
-val atomize_rules = thms "atomize'";
-val atomize_tac = Method.atomize_tac atomize_rules;
-val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
-
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
@@ -51,7 +47,6 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= atomize_rules
   end;
 
 structure Classical = ClassicalFun(Classical_Data);