# HG changeset patch
# User wenzelm
# Date 1237840812 -3600
# Node ID 2f17c664d7fa095550026c1ec2ba2ce42be2caf6
# Parent  60568c168040507db37319b42452af737da54f43
removed obsolete ml_output;

diff -r 60568c168040 -r 2f17c664d7fa src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/General/output.ML	Mon Mar 23 21:40:12 2009 +0100
@@ -47,7 +47,6 @@
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
-  val ml_output: (string -> unit) * (string -> 'a)
   val accumulated_time: unit -> unit
 end;
 
@@ -120,8 +119,6 @@
 val debugging = ref false;
 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
 
-val ml_output = (writeln, error);
-
 
 
 (** timing **)