--- a/Nominal/Rsp.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -146,6 +146,34 @@
 by auto
 
 ML {*
+  fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+  fun all_eqvts ctxt =
+    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
+  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+ML {*
+fun mk_minimal_ss ctxt =
+  Simplifier.context ctxt empty_ss
+    setsubgoaler asm_simp_tac
+    setmksimps (mksimps [])
+*}
+
+ML {*
+fun alpha_eqvt_tac induct simps ctxt =
+  indtac induct THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
+  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps 
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW
+  (split_conjs THEN_ALL_NEW TRY o resolve_tac
+    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
+  THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt))
+*}
+
+ML {*
 fun build_alpha_eqvts funs perms simps induct ctxt =
 let
   val pi = Free ("p", @{typ perm});
@@ -158,17 +186,7 @@
     HOLogic.mk_imp (alpha $ arg $ arg2,
       (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (
-   (asm_full_simp_tac (HOL_ss addsimps 
-      ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))
-    THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN'
-      REPEAT o etac conjE THEN'
-      (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
-      (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))))) 1
+  fun tac _ = alpha_eqvt_tac induct simps ctxt 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)