changeset 2170 | 1fe84fd8f8a4 |
parent 2168 | ce0255ffaeb4 |
child 2301 | 8732ff59068b |
--- a/Nominal-General/nominal_permeq.ML Fri May 21 10:47:07 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Fri May 21 10:47:45 2010 +0200 @@ -155,7 +155,7 @@ (** methods **) -val _ = OuterKeyword.keyword "exclude" +val _ = Keyword.keyword "exclude" val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- (Scan.repeat (Args.const true))) []