# HG changeset patch
# User wenzelm
# Date 1273670758 -7200
# Node ID 7330e4eefbd789d6803597aa88ac6ac959e5da56
# Parent  116be5acd5a750f3530d8ebcccd9861da289f192
updated/unified some legacy warnings;

diff -r 116be5acd5a7 -r 7330e4eefbd7 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed May 12 15:23:38 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Wed May 12 15:25:58 2010 +0200
@@ -326,7 +326,8 @@
     || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
       Toplevel.theory (snd o
         (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
-          alt_name (map P.triple_swap eqns)))));
+          alt_name (map P.triple_swap eqns) o
+        tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
 
 end;
 
diff -r 116be5acd5a7 -r 7330e4eefbd7 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed May 12 15:23:38 2010 +0200
+++ b/src/HOL/Tools/recdef.ML	Wed May 12 15:25:58 2010 +0200
@@ -184,7 +184,7 @@
 
 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
   let
-    val _ = legacy_feature ("\"recdef\"; prefer \"function\" instead");
+    val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead";
     val _ = requires_recdef thy;
 
     val name = Sign.intern_const thy raw_name;
diff -r 116be5acd5a7 -r 7330e4eefbd7 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Wed May 12 15:23:38 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Wed May 12 15:25:58 2010 +0200
@@ -427,7 +427,7 @@
 
 fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
   let
-    val _ = legacy_feature "\"fixpat\"; prefer \"fixrec_simp\" method instead";
+    val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead";
     val atts = map (prep_attrib thy) srcs;
     val ts = map (prep_term thy) strings;
     val simps = map (fix_pat thy) ts;
diff -r 116be5acd5a7 -r 7330e4eefbd7 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed May 12 15:23:38 2010 +0200
+++ b/src/Pure/Isar/constdefs.ML	Wed May 12 15:25:58 2010 +0200
@@ -22,7 +22,7 @@
 fun gen_constdef prep_vars prep_prop prep_att
     structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
   let
-    val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead");
+    val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead";
 
     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
 
diff -r 116be5acd5a7 -r 7330e4eefbd7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed May 12 15:23:38 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 12 15:25:58 2010 +0200
@@ -181,7 +181,10 @@
 
 val _ =
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
-    (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
+    (Scan.repeat1 SpecParse.spec >>
+      (Toplevel.theory o
+        (IsarCmd.add_axioms o
+          tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
 
 val opt_unchecked_overloaded =
   Scan.optional (P.$$$ "(" |-- P.!!!