non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;

--- a/src/Pure/General/output.ML	Fri Aug 27 22:30:25 2010 +0200
+++ b/src/Pure/General/output.ML	Sat Aug 28 15:25:32 2010 +0200
@@ -79,11 +79,8 @@
 
 (* output primitives -- normally NOT used directly!*)
 
-fun std_output s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
-
-fun std_error s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
+fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
 fun writeln_default "" = ()
   | writeln_default s = std_output (suffix "\n" s);