--- a/src/HOL/Nominal/nominal_primrec.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon Apr 06 17:06:48 2015 +0200
@@ -403,7 +403,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
"define primitive recursive functions on nominal datatypes"
(options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>