--- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 16 18:20:12 2012 +0100
@@ -402,8 +402,8 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
val _ =
- Outer_Syntax.local_theory_to_proof "nominal_primrec"
- "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
+ Outer_Syntax.local_theory_to_proof @{command_spec "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) =>
add_primrec_cmd invs fctxt fixes params specs));