# HG changeset patch
# User wenzelm
# Date 1003082645 -7200
# Node ID 3928d990c22ff81f97eef70588d4c476af30f89f
# Parent  02b257ef0ee26e6aab99de139fdb48f560c76ae8
ObjectLogic.atomize_tac;

diff -r 02b257ef0ee2 -r 3928d990c22f src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Oct 14 20:02:59 2001 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Oct 14 20:04:05 2001 +0200
@@ -238,7 +238,7 @@
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
         val (tac, _) = foldl mk_unique_tac
-          (((rtac induct' THEN_ALL_NEW atomize_strip_tac) 1, rec_intrs),
+          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1, rec_intrs),
             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
 
       in split_conj_thm (prove_goalw_cterm []
diff -r 02b257ef0ee2 -r 3928d990c22f src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Oct 14 20:02:59 2001 +0200
+++ b/src/Provers/blast.ML	Sun Oct 14 20:04:05 2001 +0200
@@ -67,7 +67,6 @@
 		 uwrappers: (string * wrapper) list,
 		 safe0_netpair: netpair, safep_netpair: netpair,
 		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
-  val atomize: thm list
   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   end;
@@ -117,7 +116,6 @@
 struct
 
 type claset = Data.claset;
-val atomize_goal = Method.atomize_goal Data.atomize;
 
 val trace = ref false
 and stats = ref false;   (*for runtime and search statistics*)
@@ -1277,7 +1275,7 @@
  "lim" is depth limit.*)
 fun timing_depth_tac start cs lim i st0 = 
  (initialize();
-  let val st = atomize_goal i st0;
+  let val st = ObjectLogic.atomize_goal i st0;
       val {sign,...} = rep_thm st
       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
       val hyps  = strip_imp_prems skoprem
diff -r 02b257ef0ee2 -r 3928d990c22f src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Oct 14 20:02:59 2001 +0200
+++ b/src/Provers/classical.ML	Sun Oct 14 20:04:05 2001 +0200
@@ -33,7 +33,6 @@
   val classical : thm           (* (~P ==> P) ==> P *)
   val sizef     : thm -> int    (* size function for BEST_FIRST *)
   val hyp_subst_tacs: (int -> tactic) list
-  val atomize: thm list
 end;
 
 signature BASIC_CLASSICAL =
@@ -182,8 +181,6 @@
 
 (*** Useful tactics for classical reasoning ***)
 
-val atomize_tac = Method.atomize_tac atomize;
-
 val imp_elim = (*cannot use bind_thm within a structure!*)
   store_thm ("imp_elim", Data.make_elim mp);
 
@@ -837,24 +834,24 @@
 
 (*Dumb but fast*)
 fun fast_tac cs =
-  atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+  ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
 
 (*Slower but smarter than fast_tac*)
 fun best_tac cs =
-  atomize_tac THEN'
+  ObjectLogic.atomize_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
 
 (*even a bit smarter than best_tac*)
 fun first_best_tac cs =
-  atomize_tac THEN'
+  ObjectLogic.atomize_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
 
 fun slow_tac cs =
-  atomize_tac THEN'
+  ObjectLogic.atomize_tac THEN'
   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
 
 fun slow_best_tac cs =
-  atomize_tac THEN'
+  ObjectLogic.atomize_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
 
 
@@ -862,13 +859,13 @@
 val weight_ASTAR = ref 5;
 
 fun astar_tac cs =
-  atomize_tac THEN'
+  ObjectLogic.atomize_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
       (step_tac cs 1));
 
 fun slow_astar_tac cs =
-  atomize_tac THEN'
+  ObjectLogic.atomize_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
       (slow_step_tac cs 1));