src/Pure/General/output.ML
changeset 24652 22b657bee22d
parent 24612 d1b315bdb8d7
child 25640 1546ffd84986
--- a/src/Pure/General/output.ML	Wed Sep 19 18:48:54 2007 +0200
+++ b/src/Pure/General/output.ML	Wed Sep 19 20:45:29 2007 +0200
@@ -46,7 +46,7 @@
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
   val error_msg: string -> unit
-  val ml_output: (string -> unit) * (string -> unit)
+  val ml_output: (string -> unit) * (string -> 'a)
   val accumulated_time: unit -> unit
 end;
 
@@ -117,7 +117,7 @@
 
 fun error_msg s = ! error_fn (output s);
 
-val ml_output = (writeln, error_msg);
+val ml_output = (writeln, error);