src/Pure/General/print_mode.ML
changeset 33223 d27956b4d3b4
parent 32738 15bb09ca0378
child 37146 f652333bbf8e
--- a/src/Pure/General/print_mode.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/General/print_mode.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -35,7 +35,7 @@
   let val modes =
     (case Thread.getLocal tag of
       SOME (SOME modes) => modes
-    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
+    | _ => ! print_mode)
   in subtract (op =) [input, internal] modes end;
 
 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;