diff -r a549dc15c037 -r 5f859035331f src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Mar 06 22:47:32 2009 +0100
+++ b/src/Pure/General/output.ML	Fri Mar 06 22:50:30 2009 +0100
@@ -32,7 +32,6 @@
   val escape: output -> string
   val std_output: output -> unit
   val std_error: output -> unit
-  val immediate_output: string -> unit
   val writeln_default: output -> unit
   val writeln_fn: (output -> unit) ref
   val priority_fn: (output -> unit) ref
@@ -89,8 +88,6 @@
 fun std_error s = NAMED_CRITICAL "IO" (fn () =>
   (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
 
-val immediate_output = std_output o output;
-
 fun writeln_default "" = ()
   | writeln_default s = std_output (suffix "\n" s);