--- a/src/Pure/General/output.ML Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/General/output.ML Thu Dec 13 19:53:55 2012 +0100
@@ -45,7 +45,6 @@
val report: string -> unit
val result: serial * string -> unit
val protocol_message: Properties.T -> string -> unit
- exception TRACING_LIMIT of int
end;
structure Output: OUTPUT =
@@ -116,8 +115,6 @@
fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
-exception TRACING_LIMIT of int;
-
end;
structure Basic_Output: BASIC_OUTPUT = Output;