diff -r cbcd4997dac5 -r 22a084c9316b Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -136,6 +136,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 +155,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 (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