# HG changeset patch
# User wenzelm
# Date 1185394847 -7200
# Node ID 83e6e9ad0f4f9745071ef5c23646940e2ee96b72
# Parent  aaff3bc5ec28736c44b2ab2d9e4e86c613bcace3
NAMED_CRITICAL;

diff -r aaff3bc5ec28 -r 83e6e9ad0f4f src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Jul 25 18:10:49 2007 +0200
+++ b/src/Provers/blast.ML	Wed Jul 25 22:20:47 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 = CRITICAL (fn () =>
+fun timing_depth_tac start cs lim i st0 = NAMED_CRITICAL "blast" (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))