diff -r a5dc3558cdec -r ce0255ffaeb4 Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_permeq.ML	Fri May 21 10:42:53 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))) []