src/ZF/Tools/primrec_package.ML

 
 
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
-    Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
     (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
       >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
 
 end;