diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Fri Apr 16 16:29:11 2010 +0200
@@ -86,22 +86,28 @@
 
 (** equivariance tactics **)
 
+val perm_boolE = @{thm permute_boolE}
+val perm_cancel = @{thms permute_minus_cancel(2)}
+val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def}
+
 fun eqvt_rel_case_tac ctxt pred_names pi intro  = 
 let
   val thy = ProofContext.theory_of ctxt
   val cpi = Thm.cterm_of thy (mk_minus pi)
-  val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE}
-  val permute_cancel = @{thms permute_minus_cancel(2)}
+  val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
+  val simps = HOL_basic_ss addsimps perm_expand_bool
 in
-  eqvt_strict_tac ctxt [] [] THEN' 
-  SUBPROOF (fn {prems, context, ...} =>
+  eqvt_strict_tac ctxt [] pred_names THEN' 
+  SUBPROOF (fn {prems, context as ctxt, ...} =>
     let
       val prems' = map (transform_prem ctxt pred_names) prems
-      val side_cond_tac = EVERY' 
-        [ rtac rule, eqvt_strict_tac context permute_cancel [],
-          resolve_tac prems' ]
+      val tac1 = resolve_tac prems'
+      val tac2 = EVERY' [ rtac pi_intro_rule, 
+            eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
+      val tac3 = EVERY' [ rtac pi_intro_rule, 
+            eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems']
     in
-      (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1 
+      (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 
     end) ctxt
 end