src/Pure/General/output.ML

--- a/src/Pure/General/output.ML	Mon Jul 23 19:45:45 2007 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 23 19:45:46 2007 +0200
@@ -221,7 +221,7 @@
 
 fun time_accumulator name =
   let val ti = time_init name in
-    change time_finish_hooks (cons (fn () => time_finish ti));
+    CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
     time_add ti
   end;