--- a/Nominal/nominal_eqvt.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_eqvt.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -5,6 +5,7 @@
     Automatic proofs for equivariance of inductive predicates.
 *)
 
+
 signature NOMINAL_EQVT =
 sig
   val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
@@ -32,7 +33,6 @@
 (** equivariance tactics **)
 
 val perm_boolE = @{thm permute_boolE}
-val perm_cancel = @{thms permute_minus_cancel(2)}
 
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
   let
@@ -41,16 +41,18 @@
     val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
     val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all}
     val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def}
+    val eqvt_sconfig = 
+          eqvt_strict_config addpres @{thms permute_minus_cancel(2)} addexcls pred_names
   in
-    eqvt_strict_tac ctxt [] pred_names THEN'
+    eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN'
     SUBPROOF (fn {prems, context as ctxt, ...} =>
       let
         val prems' = map (transform_prem2 ctxt pred_names) prems
         val tac1 = resolve_tac prems'
         val tac2 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
+          eqvt_tac ctxt eqvt_sconfig, resolve_tac prems' ]
         val tac3 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, 
+          eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, 
           simp_tac simps2, resolve_tac prems']
       in
         (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1