--- a/Nominal-General/nominal_permeq.ML	Sun Apr 25 08:18:06 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Sun Apr 25 09:13:16 2010 +0200
@@ -7,6 +7,11 @@
 sig
   val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
   val eqvt_strict_tac: Proof.context -> thm list -> string list -> 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 args_parser: (thm list * string list) context_parser
+
   val trace_eqvt: bool Config.T
   val setup: theory -> theory
 end;
@@ -157,4 +162,21 @@
 val setup =
   trace_eqvt_setup
 
+
+(** methods **)
+
+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))) []
+
+val args_parser =  
+  add_thms_parser -- exclude_consts_parser ||
+  exclude_consts_parser -- add_thms_parser >> swap
+
+fun perm_simp_meth (thms, consts) ctxt = 
+  SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
+
+fun perm_strict_simp_meth (thms, consts) ctxt = 
+  SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
+
 end; (* structure *)
\ No newline at end of file