updated/unified some legacy warnings;
authorwenzelm
Wed May 12 15:25:58 2010 +0200 (2010-05-12 ago)
changeset 368657330e4eefbd7
parent 36864 116be5acd5a7
child 36866 426d5781bb25
updated/unified some legacy warnings;
src/HOL/Tools/primrec.ML
src/HOL/Tools/recdef.ML
src/HOLCF/Tools/fixrec.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/HOL/Tools/primrec.ML	Wed May 12 15:23:38 2010 +0200
     1.2 +++ b/src/HOL/Tools/primrec.ML	Wed May 12 15:25:58 2010 +0200
     1.3 @@ -326,7 +326,8 @@
     1.4      || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
     1.5        Toplevel.theory (snd o
     1.6          (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
     1.7 -          alt_name (map P.triple_swap eqns)))));
     1.8 +          alt_name (map P.triple_swap eqns) o
     1.9 +        tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
    1.10  
    1.11  end;
    1.12  
     2.1 --- a/src/HOL/Tools/recdef.ML	Wed May 12 15:23:38 2010 +0200
     2.2 +++ b/src/HOL/Tools/recdef.ML	Wed May 12 15:25:58 2010 +0200
     2.3 @@ -184,7 +184,7 @@
     2.4  
     2.5  fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
     2.6    let
     2.7 -    val _ = legacy_feature ("\"recdef\"; prefer \"function\" instead");
     2.8 +    val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead";
     2.9      val _ = requires_recdef thy;
    2.10  
    2.11      val name = Sign.intern_const thy raw_name;
     3.1 --- a/src/HOLCF/Tools/fixrec.ML	Wed May 12 15:23:38 2010 +0200
     3.2 +++ b/src/HOLCF/Tools/fixrec.ML	Wed May 12 15:25:58 2010 +0200
     3.3 @@ -427,7 +427,7 @@
     3.4  
     3.5  fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
     3.6    let
     3.7 -    val _ = legacy_feature "\"fixpat\"; prefer \"fixrec_simp\" method instead";
     3.8 +    val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead";
     3.9      val atts = map (prep_attrib thy) srcs;
    3.10      val ts = map (prep_term thy) strings;
    3.11      val simps = map (fix_pat thy) ts;
     4.1 --- a/src/Pure/Isar/constdefs.ML	Wed May 12 15:23:38 2010 +0200
     4.2 +++ b/src/Pure/Isar/constdefs.ML	Wed May 12 15:25:58 2010 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  fun gen_constdef prep_vars prep_prop prep_att
     4.5      structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
     4.6    let
     4.7 -    val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead");
     4.8 +    val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead";
     4.9  
    4.10      fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
    4.11  
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Wed May 12 15:23:38 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed May 12 15:25:58 2010 +0200
     5.3 @@ -181,7 +181,10 @@
     5.4  
     5.5  val _ =
     5.6    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
     5.7 -    (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
     5.8 +    (Scan.repeat1 SpecParse.spec >>
     5.9 +      (Toplevel.theory o
    5.10 +        (IsarCmd.add_axioms o
    5.11 +          tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
    5.12  
    5.13  val opt_unchecked_overloaded =
    5.14    Scan.optional (P.$$$ "(" |-- P.!!!