--- a/Nominal/Abs.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -114,14 +114,13 @@
   done
 
 lemma alpha_gen_compose_eqvt:
-  assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+  fixes  pia
+  assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
   and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
   and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  shows  "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)"
+  shows  "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
   using b
   apply -
-  apply(erule exE)
-  apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(rule conjI)
@@ -419,6 +418,7 @@
 apply(simp add: supp_swap)
 done
 
+(*
 thm supp_perm
 
 lemma perm_induct_test:
@@ -502,6 +502,6 @@
 apply(simp)
 oops
 
-
+*)
 end