--- a/Nominal-General/Nominal2_Eqvt.thy	Thu Apr 22 05:16:23 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu Apr 22 06:44:24 2010 +0200
@@ -249,7 +249,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  supp_eqvt fresh_eqvt
+  supp_eqvt fresh_eqvt add_perm_eqvt
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
@@ -259,8 +259,7 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
 
-  add_perm_eqvt
-
+ 
 lemmas [eqvt_raw] =
   permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
 
@@ -289,20 +288,25 @@
 setup Nominal_Permeq.setup
 
 ML {*
-val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
-val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
+val add_thms = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
+val exclude_consts = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
   (Scan.repeat (Args.const true))) []
+
+val parser =  
+  add_thms -- exclude_consts ||
+  exclude_consts -- add_thms >> swap
 *}
 
 method_setup perm_simp =
- {* test1 -- test2 >> 
-    (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
+ {* parser >> 
+      (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL 
+        (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
  {* pushes permutations inside *}
 
 method_setup perm_strict_simp =
- {* test1 -- test2 >> 
-    (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL 
-       (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
+ {* parser >> 
+      (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL 
+        (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
  {* pushes permutations inside, raises an error if it cannot solve all permutations *}
 
 declare [[trace_eqvt = true]]