# HG changeset patch
# User wenzelm
# Date 1312802994 -7200
# Node ID 00f0c8782a51d4e7cf6825cbf4c7787de64c0548
# Parent  2ec66075a75cb627b29ad1572ad850b55d2f33b2
slightly more uniform messages;

diff -r 2ec66075a75c -r 00f0c8782a51 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Aug 08 13:19:19 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Mon Aug 08 13:29:54 2011 +0200
@@ -87,7 +87,8 @@
     val defname = mk_defname fixes
     val FunctionConfig {partials, default, ...} = config
     val _ =
-      if is_some default then legacy_feature "'function (default)'. Use 'partial_function'."
+      if is_some default
+      then legacy_feature "\"function (default)\" -- use 'partial_function' instead"
       else ()
 
     val ((goal_state, cont), lthy') =
diff -r 2ec66075a75c -r 00f0c8782a51 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 08 13:19:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 08 13:29:54 2011 +0200
@@ -235,8 +235,7 @@
   let
     val _ =
       if default_type_syss = full_type_syss then
-        legacy_feature "Old 'metisFT' method -- \
-                       \use 'metis (full_types)' instead"
+        legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
       else
         ()
     val (schem_facts, nonschem_facts) = List.partition has_tvar facts
diff -r 2ec66075a75c -r 00f0c8782a51 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Aug 08 13:19:19 2011 +0200
+++ b/src/Pure/codegen.ML	Mon Aug 08 13:29:54 2011 +0200
@@ -916,7 +916,9 @@
 
 fun eval_term ctxt t =
   let
-    val _ = legacy_feature "Old evaluation mechanism -- use evaluator 'code' or method eval instead";
+    val _ =
+      legacy_feature
+        "Old evaluation mechanism -- use evaluator \"code\" or method \"eval\" instead";
     val thy = Proof_Context.theory_of ctxt;
     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
       error "Term to be evaluated contains type variables";
@@ -1013,7 +1015,7 @@
    || Scan.repeat1 (Parse.term >> pair "")) >>
   (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
     let
-      val _ = legacy_feature "Old code generation command -- use export_code instead";
+      val _ = legacy_feature "Old code generation command -- use 'export_code' instead";
       val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
       val (code, gr) = generate_code thy mode' modules module xs;
       val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>