# HG changeset patch
# User wenzelm
# Date 979601330 -3600
# Node ID de95ba2760fe6bf2212abed15ced2b0c0e1a61f4
# Parent  e23abeef8150c51f8dca92e2809704a0b1d5642d
tuned atomize;

diff -r e23abeef8150 -r de95ba2760fe src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/FOL/blastdata.ML	Tue Jan 16 00:28:50 2001 +0100
@@ -10,7 +10,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Cla.claset
   val rep_cs    = Cla.rep_cs
-  val atomize	= thms "atomize'"
+  val atomize	= atomize_rules
   val cla_modifiers = Cla.cla_modifiers;
   val cla_meth' = Cla.cla_meth'
   end;
diff -r e23abeef8150 -r de95ba2760fe src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/FOL/cladata.ML	Tue Jan 16 00:28:50 2001 +0100
@@ -15,6 +15,10 @@
   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
@@ -24,7 +28,7 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize'"
+  val atomize	= atomize_rules
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
diff -r e23abeef8150 -r de95ba2760fe src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/HOL/arith_data.ML	Tue Jan 16 00:28:50 2001 +0100
@@ -407,8 +407,6 @@
 *)
 local
 
-val atomize_tac = Method.atomize_tac (thms "atomize'");
-
 fun raw_arith_tac i st =
   refute_tac (K true) (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
              ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
diff -r e23abeef8150 -r de95ba2760fe src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/HOL/blastdata.ML	Tue Jan 16 00:28:50 2001 +0100
@@ -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	= thms "atomize'"
+  val atomize	= atomize_rules
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;
diff -r e23abeef8150 -r de95ba2760fe src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/HOL/cladata.ML	Tue Jan 16 00:28:50 2001 +0100
@@ -38,6 +38,10 @@
   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
@@ -47,7 +51,7 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize'"
+  val atomize	= atomize_rules
   end;
 
 structure Classical = ClassicalFun(Classical_Data);