diff -r bd774e01d6d5 -r 0f4c501a691e src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Apr 30 13:22:35 2007 +0200
+++ b/src/Pure/General/output.ML	Mon Apr 30 13:32:58 2007 +0200
@@ -11,6 +11,8 @@
   val priority: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
+  val tolerate_legacy_features: bool ref
+  val legacy_feature: string -> unit
   val timing: bool ref
   val cond_timeit: bool -> (unit -> 'a) -> 'a
   val timeit: (unit -> 'a) -> 'a
@@ -110,6 +112,10 @@
 fun tracing s = ! tracing_fn (output s);
 fun warning s = ! warning_fn (output s);
 
+val tolerate_legacy_features = ref true;
+fun legacy_feature s =
+  (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s);
+
 fun no_warnings f = setmp warning_fn (K ()) f;
 
 val debugging = ref false;