diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_permeq.ML
--- a/Nominal/nominal_permeq.ML	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_permeq.ML	Thu Mar 13 09:21:31 2014 +0000
@@ -22,8 +22,8 @@
   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic
 
-  val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
-  val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
+  val perm_simp_meth: thm list * string list -> Proof.context -> Proof.method
+  val perm_strict_simp_meth: thm list * string list -> Proof.context -> Proof.method
   val args_parser: (thm list * string list) context_parser
 
   val trace_eqvt: bool Config.T
@@ -219,9 +219,9 @@
    Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];
 
 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
-  (Scan.repeat (Args.const true))) []
+  (Scan.repeat (Args.const {proper = true, strict = true}))) []
 
-val args_parser =  add_thms_parser -- exclude_consts_parser 
+val args_parser = add_thms_parser -- exclude_consts_parser 
 
 fun perm_simp_meth (thms, consts) ctxt =
   SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts)))