--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 30 14:15:44 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 30 20:58:16 2016 +0200
@@ -687,8 +687,7 @@
val _ = Outer_Syntax.local_theory @{command_keyword primrec}
"define primitive recursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
- --| @{keyword ")"}) []) --
- (Parse.fixes -- Parse_Spec.where_multi_specs)
+ --| @{keyword ")"}) []) -- Parse_Spec.specification
>> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
end;