1.1 --- a/src/HOL/Tools/primrec.ML	Tue Sep 28 12:48:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/primrec.ML	Tue Sep 28 15:32:59 2010 +0200
     1.3 @@ -320,12 +320,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
     1.6    Keyword.thy_decl
     1.7 -    ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
     1.8 -      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
     1.9 -    || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
    1.10 -      Toplevel.theory (snd o
    1.11 -        (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
    1.12 -          alt_name (map Parse.triple_swap eqns) o
    1.13 -        tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
    1.14 +    (primrec_decl >> (fn ((opt_target, fixes), specs) =>
    1.15 +      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)));
    1.16  
    1.17  end;