# HG changeset patch
# User wenzelm
# Date 973547261 -3600
# Node ID 8621cb0021a648784a8eb308742b5220116251b1
# Parent  e37e123738f75c66f685c2a446ec126445d59d23
tuned atomize_goal;

diff -r e37e123738f7 -r 8621cb0021a6 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Nov 06 18:28:22 2000 +0100
+++ b/src/Provers/blast.ML	Mon Nov 06 22:47:41 2000 +0100
@@ -116,6 +116,7 @@
 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*)
@@ -1273,7 +1274,7 @@
  "lim" is depth limit.*)
 fun timing_depth_tac start cs lim i st0 = 
  (initialize();
-  let val st = Method.atomize_goal Data.atomize i st0;
+  let val st = 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