--- a/src/Pure/General/output.ML Sat Aug 27 16:22:59 2011 +0200
+++ b/src/Pure/General/output.ML Sat Aug 27 17:26:14 2011 +0200
@@ -9,7 +9,6 @@
val writeln: string -> unit
val tracing: string -> unit
val warning: string -> unit
- val legacy_feature: string -> unit
end;
signature OUTPUT =
@@ -113,8 +112,6 @@
fun report s = ! Private_Hooks.report_fn (output s);
fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
-fun legacy_feature s = warning ("Legacy feature! " ^ s);
-
end;
structure Basic_Output: BASIC_OUTPUT = Output;