--- a/src/HOL/Tools/Datatype/primrec.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Tools/Datatype/primrec.ML Fri Mar 16 18:20:12 2012 +0100
@@ -310,8 +310,8 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory "primrec" "define primitive recursive functions on datatypes"
- Keyword.thy_decl
+ Outer_Syntax.local_theory @{command_spec "primrec"}
+ "define primitive recursive functions on datatypes"
(Parse.fixes -- Parse_Spec.where_alt_specs
>> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd));