--- 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 **)