--- a/Nominal/Rsp.thy	Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -78,8 +78,12 @@
 ML {*
 fun fvbv_rsp_tac induct fvbv_simps =
   ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac
-  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))
+  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW
+  asm_full_simp_tac
+  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))
+  THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN'
+  asm_full_simp_tac
+  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))))
 *}
 
 ML {*
@@ -136,6 +140,10 @@
 end
 *}
 
+lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="pi \<bullet> pia" in exI)
+by auto
 
 ML {*
 fun build_alpha_eqvts funs perms simps induct ctxt =
@@ -151,18 +159,20 @@
       (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 
+  (
+   (asm_full_simp_tac (HOL_ss addsimps 
       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
+    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 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
 end
 *}
 
-
 end