--- a/src/Pure/General/output.ML Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/output.ML Sun Jul 29 17:28:55 2007 +0200
@@ -82,10 +82,10 @@
(* output primitives -- normally NOT used directly!*)
-fun std_output s = CRITICAL (fn () =>
+fun std_output s = NAMED_CRITICAL "IO" (fn () =>
(TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
-fun std_error s = CRITICAL (fn () =>
+fun std_error s = NAMED_CRITICAL "IO" (fn () =>
(TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
val immediate_output = std_output o output;