src/HOL/Tools/BNF/bnf_def.ML
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;