changeset 58660 | 8d4aebb9e327 |
parent 58659 | 6c9821c32dd5 |
child 58893 | 9e0ecb66d6a7 |
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Oct 13 18:45:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Oct 13 19:34:10 2014 +0200 @@ -1614,7 +1614,7 @@ Scan.repeat1 (Scan.unless (Parse.reserved "rel" || Parse.reserved "plugins") Parse.term)) [] -- Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) -- - Scan.optional Plugin_Name.parse_filter (K (K true)) + Scan.optional Plugin_Name.parse_filter (K Plugin_Name.default_filter) >> bnf_cmd); end;