# HG changeset patch
# User blanchet
# Date 1411569342 -7200
# Node ID 121d5e3319eee5a41ca166c037b756e3e5a87b96
# Parent  751e8517daa78dcde1a12f01aa0d7ef46faf2290
improved 'bnf' parser

diff -r 751e8517daa7 -r 121d5e3319ee src/HOL/Tools/BNF/bnf_def.ML
--- 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);