src/Pure/General/output.ML

--- a/src/Pure/General/output.ML	Mon Jul 12 22:14:11 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 12 22:17:31 2010 +0200
@@ -11,7 +11,6 @@
   val priority: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
-  val tolerate_legacy_features: bool Unsynchronized.ref
   val legacy_feature: string -> unit
   val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
   val timeit: (unit -> 'a) -> 'a
@@ -108,9 +107,7 @@
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn (output s);
 
-val tolerate_legacy_features = Unsynchronized.ref true;
-fun legacy_feature s =
-  (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
+fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
 fun no_warnings_CRITICAL f = setmp_CRITICAL warning_fn (K ()) f;