--- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 16 18:20:12 2012 +0100
@@ -402,7 +402,7 @@
in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
val _ =
- Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
+ Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
(Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
>> (fn (fixes, specs) => add_fixrec_cmd fixes specs))