# 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);