--- a/Nominal-General/nominal_eqvt.ML	Sun May 09 11:37:19 2010 +0100
+++ b/Nominal-General/nominal_eqvt.ML	Sun May 09 11:43:24 2010 +0100
@@ -52,9 +52,10 @@
 fun map_thm_tac ctxt tac thm =
 let
   val monos = Inductive.get_monos ctxt
+  val simps = HOL_basic_ss addsimps @{thms split_def}
 in
-  EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
-    REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
+  EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
+    REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
     REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
 end
 
@@ -89,25 +90,25 @@
 
 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_single_case_tac ctxt pred_names pi intro  = 
 let
   val thy = ProofContext.theory_of ctxt
   val cpi = Thm.cterm_of thy (mk_minus pi)
   val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
-  val simps = HOL_basic_ss addsimps perm_expand_bool
+  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}
 in
-  eqvt_strict_tac ctxt [] pred_names THEN' 
+  eqvt_strict_tac ctxt [] pred_names THEN'
   SUBPROOF (fn {prems, context as ctxt, ...} =>
     let
       val prems' = map (transform_prem 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' ]
       val tac3 = EVERY' [ rtac pi_intro_rule, 
-            eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems']
+            eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, 
+            simp_tac simps2, resolve_tac prems']
     in
       (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 
     end) ctxt