--- a/Nominal/nominal_eqvt.ML	Wed Dec 21 17:05:00 2011 +0900
+++ b/Nominal/nominal_eqvt.ML	Thu Dec 22 04:35:01 2011 +0000
@@ -28,30 +28,24 @@
 
 (** equivariance tactics **)
 
-val perm_boolE = @{thm permute_boolE}
-
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
   let
     val thy = Proof_Context.theory_of ctxt
-    val cpi = Thm.cterm_of thy (mk_minus pi)
-    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
+    val cpi = Thm.cterm_of thy pi
+    val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
+    val eqvt_sconfig = eqvt_strict_config addexcls pred_names
+    val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all}
+    val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def  permute_minus_cancel(2)}
   in
-    eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN'
+    eqvt_tac ctxt eqvt_sconfig 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_tac ctxt eqvt_sconfig, resolve_tac prems' ]
-        val tac3 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, 
-          simp_tac simps2, resolve_tac prems']
+        val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems'
+        val prems''' = map (simplify simps2 o simplify simps1) prems''
+
       in
-        (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 
+        HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) 
       end) ctxt
   end