# HG changeset patch
# User wenzelm
# Date 1003082395 -7200
# Node ID 06eb315831ffcd998b2904feaee5a12aedac9628
# Parent  17a6dcd6f3cf178bf2ac6263592cc4dcd0b17d41
eliminated atomize rules;

diff -r 17a6dcd6f3cf -r 06eb315831ff src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Sun Oct 14 19:59:15 2001 +0200
+++ b/src/FOL/blastdata.ML	Sun Oct 14 19:59:55 2001 +0200
@@ -10,7 +10,6 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Cla.claset
   val rep_cs    = Cla.rep_cs
-  val atomize	= atomize_rules
   val cla_modifiers = Cla.cla_modifiers;
   val cla_meth' = Cla.cla_meth'
   end;
diff -r 17a6dcd6f3cf -r 06eb315831ff src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Sun Oct 14 19:59:15 2001 +0200
+++ b/src/FOL/cladata.ML	Sun Oct 14 19:59:55 2001 +0200
@@ -15,10 +15,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
@@ -28,7 +24,6 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= atomize_rules
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
diff -r 17a6dcd6f3cf -r 06eb315831ff 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