# HG changeset patch
# User wenzelm
# Date 1185299069 -7200
# Node ID bb838771157f4b654bead5325cb0978c541a49aa
# Parent  54fab60ddc970b69dca1e3d03e9342ba8eaa80ca
marked some CRITICAL sections;

diff -r 54fab60ddc97 -r bb838771157f src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Jul 24 15:29:57 2007 +0200
+++ b/src/Provers/blast.ML	Tue Jul 24 19:44:29 2007 +0200
@@ -1246,7 +1246,7 @@
  "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 st0 =
+fun timing_depth_tac start cs lim i st0 = CRITICAL (fn () =>
   let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
       val sign = Thm.theory_of_thm st
       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
@@ -1266,9 +1266,10 @@
                        else ();
                        Seq.make(fn()=> cell))
           end
-  in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
-  end
-  handle PROVE     => Seq.empty;
+      val forced = Seq.pull
+        (prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont))
+  in Seq.make (fn () => forced) end
+  handle PROVE     => Seq.empty);
 
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;