# HG changeset patch
# User wenzelm
# Date 1190227529 -7200
# Node ID 22b657bee22d5301cd9cd78fec08f5f50d911495
# Parent  452962f294a3ce423cba9199ec181f2fd29195ff
ml_output: proper error instead of error_msg;

diff -r 452962f294a3 -r 22b657bee22d src/Pure/General/output.ML
--- 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);