removed obsolete ml_output;
authorwenzelm
Mon, 23 Mar 2009 21:40:12 +0100
changeset 30674 2f17c664d7fa
parent 30673 60568c168040
child 30675 2e796219f441
removed obsolete ml_output;
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 **)