--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Apr 06 17:06:48 2015 +0200
@@ -669,7 +669,7 @@
|| Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
|| Parse.reserved "transfer" >> K Transfer_Option);
-val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
+val _ = Outer_Syntax.local_theory @{command_keyword primrec}
"define primitive recursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
--| @{keyword ")"}) []) --