# HG changeset patch
# User wenzelm
# Date 1278965851 -7200
# Node ID 1d639d28832c9311a668121d94680b44d18e8c23
# Parent  95aa0afcb240c6c0ed12d8b57655e3b53ca7713d
removed impractical tolerate_legacy_features flag;

diff -r 95aa0afcb240 -r 1d639d28832c 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;