# HG changeset patch
# User wenzelm
# Date 965123829 -7200
# Node ID 2df511ebb95676d4a7ef6e728ba5d3a4ea286618
# Parent  e56577a6300565c621480cd1ca832dd899c5c169
handle actual object-logic rules by atomizing the goal;

diff -r e56577a63005 -r 2df511ebb956 src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Tue Aug 01 11:55:27 2000 +0200
+++ b/src/FOL/blastdata.ML	Tue Aug 01 11:57:09 2000 +0200
@@ -10,6 +10,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Cla.claset
   val rep_cs    = Cla.rep_cs
+  val atomize	= [thm "all_eq", thm "imp_eq"]
   val cla_modifiers = Cla.cla_modifiers;
   val cla_meth' = Cla.cla_meth'
   end;
diff -r e56577a63005 -r 2df511ebb956 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Tue Aug 01 11:55:27 2000 +0200
+++ b/src/HOL/blastdata.ML	Tue Aug 01 11:57:09 2000 +0200
@@ -23,6 +23,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
+  val atomize	= [thm "all_eq", thm "imp_eq"]
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;
diff -r e56577a63005 -r 2df511ebb956 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Aug 01 11:55:27 2000 +0200
+++ b/src/Provers/blast.ML	Tue Aug 01 11:57:09 2000 +0200
@@ -67,6 +67,7 @@
 		 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;
@@ -1270,9 +1271,10 @@
  "start" is CPU time at start, for printing SEARCH time
 	(also prints reconstruction time)
  "lim" is depth limit.*)
-fun timing_depth_tac start cs lim i st = 
+fun timing_depth_tac start cs lim i st0 = 
  (initialize();
-  let val {sign,...} = rep_thm st
+  let val st = Method.atomize_goal Data.atomize i st0;
+      val {sign,...} = rep_thm st
       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem