explicit treatment of legacy_features;

--- a/NEWS	Mon Apr 30 13:22:35 2007 +0200
+++ b/NEWS	Mon Apr 30 13:32:58 2007 +0200
@@ -6,6 +6,10 @@
 
 *** General ***
 
+* More uniform information about legacy features, notably a
+warning/error of "Legacy feature: ...", depending on the state of the
+tolerate_legacy_features flag (default true).
+
 * Theory syntax: the header format ``theory A = B + C:'' has been
 discontinued in favour of ``theory A imports B C begin''.  Use isatool
 fixheaders to convert existing theory files.  INCOMPATIBILITY.

--- a/src/Provers/induct_method.ML	Mon Apr 30 13:22:35 2007 +0200
+++ b/src/Provers/induct_method.ML	Mon Apr 30 13:32:58 2007 +0200
@@ -95,7 +95,7 @@
 fun make_cases is_open rule =
   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
 
-fun warn_open true = warning "Encountered open rule cases -- deprecated"
+fun warn_open true = legacy_feature "open rule cases in proof method"
   | warn_open false = ();
 
 

--- 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;

--- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 30 13:22:35 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 30 13:32:58 2007 +0200
@@ -268,7 +268,7 @@
     if is_none (ThyLoad.check_file NONE path) then ()
     else
       let
-        val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
+        val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
         val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
         val tr_name = if time then "time_use" else "use";
       in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end

--- a/src/Pure/Syntax/mixfix.ML	Mon Apr 30 13:22:35 2007 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Mon Apr 30 13:32:58 2007 +0200
@@ -105,7 +105,7 @@
 
 val strip_esc = implode o strip o Symbol.explode;
 
-fun deprecated c = (warning ("Unnamed infix operator " ^ quote c ^ " -- deprecated"); c);
+fun deprecated c = (legacy_feature ("unnamed infix operator " ^ quote c); c);
 
 fun type_name t (InfixName _) = t
   | type_name t (InfixlName _) = t

--- a/src/Pure/old_goals.ML	Mon Apr 30 13:22:35 2007 +0200
+++ b/src/Pure/old_goals.ML	Mon Apr 30 13:32:58 2007 +0200
@@ -152,7 +152,7 @@
 *)
 fun prepare_proof atomic rths chorn =
   let
-      val _ = warning "Obsolete goal command encountered";
+      val _ = legacy_feature "old goal command";
       val {thy, t=horn,...} = rep_cterm chorn;
       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
       val (As, B) = Logic.strip_horn horn;
@@ -373,7 +373,7 @@
 (*simple version with minimal amount of checking and postprocessing*)
 fun simple_prove_goal_cterm G f =
   let
-    val _ = warning "Obsolete goal command encountered";
+    val _ = legacy_feature "old goal command";
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
     val asms = map Assumption.assume As;