diff -r f19e5837ad69 -r 5c6955f487e5 src/HOL/Tools/Datatype/primrec.ML
--- 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));