tuned messages;

--- a/src/Pure/General/output.ML	Sat Mar 15 22:07:31 2008 +0100
+++ b/src/Pure/General/output.ML	Sat Mar 15 22:07:32 2008 +0100
@@ -111,7 +111,7 @@
 
 val tolerate_legacy_features = ref true;
 fun legacy_feature s =
-  (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s);
+  (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
 
 fun no_warnings f = setmp warning_fn (K ()) f;
 

--- a/src/Pure/Isar/method.ML	Sat Mar 15 22:07:31 2008 +0100
+++ b/src/Pure/Isar/method.ML	Sat Mar 15 22:07:32 2008 +0100
@@ -222,7 +222,7 @@
 
 fun legacy_tac st =
   (legacy_feature
-      ("implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ()));
+      ("Implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ()));
     all_tac st);
 
 fun assm_tac ctxt =

--- a/src/Pure/Isar/outer_syntax.ML	Sat Mar 15 22:07:31 2008 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Mar 15 22:07:32 2008 +0100
@@ -283,7 +283,7 @@
     if is_none (ThyLoad.check_file dir path) then ()
     else
       let
-        val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
+        val _ = legacy_feature ("Loading attached ML script " ^ quote (Path.implode path));
         val tr = Toplevel.imperative (fn () =>
           ML_Context.setmp (SOME (Context.Theory (ThyInfo.get_theory name)))
             (fn () => ThyInfo.load_file time path) ());

--- a/src/Pure/Syntax/mixfix.ML	Sat Mar 15 22:07:31 2008 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Sat Mar 15 22:07:32 2008 +0100
@@ -104,7 +104,7 @@
 
 val strip_esc = implode o strip o Symbol.explode;
 
-fun deprecated c = (legacy_feature ("unnamed infix operator " ^ quote c); 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	Sat Mar 15 22:07:31 2008 +0100
+++ b/src/Pure/old_goals.ML	Sat Mar 15 22:07:32 2008 +0100
@@ -150,7 +150,7 @@
 *)
 fun prepare_proof atomic rths chorn =
   let
-      val _ = legacy_feature "old goal command";
+      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;
@@ -376,7 +376,7 @@
 (*simple version with minimal amount of checking and postprocessing*)
 fun simple_prove_goal_cterm G f =
   let
-    val _ = legacy_feature "old goal command";
+    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;

--- a/src/Tools/induct.ML	Sat Mar 15 22:07:31 2008 +0100
+++ b/src/Tools/induct.ML	Sat Mar 15 22:07:32 2008 +0100
@@ -309,7 +309,7 @@
   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
 
 fun warn_open true =
-      legacy_feature ("open rule cases in proof method" ^ Position.str_of (Position.thread_data ()))
+      legacy_feature ("Open rule cases in proof method" ^ Position.str_of (Position.thread_data ()))
   | warn_open false = ();