--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Sep 24 15:46:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Sep 24 16:35:42 2014 +0200
@@ -1616,7 +1616,8 @@
Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) [] --|
(Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term --
Scan.optional ((Parse.reserved "wits" -- @{keyword ":"}) |--
- Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) [] --
+ Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
+ Parse.reserved "plugins") Parse.term)) [] --
Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
Scan.optional parse_plugins (K true)
>> bnf_cmd);