diff -r 3d68573e46d3 -r b71b838b0a75 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri Apr 16 10:47:13 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 11:09:32 2010 +0200
@@ -183,7 +183,7 @@
   a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
 | a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
-| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
+| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
 declare permute_lam_raw.simps[eqvt]
@@ -203,10 +203,24 @@
 apply(rule a2)
 apply(simp)
 apply(simp)
-apply(perm_simp)
-apply(rule a3)
-apply(unfold alpha_gen)
-oops
+
+apply simp
+apply (rule a3)
+apply (erule exi[of _ _ "p"])
+apply (simp add: alphas)
+apply (erule conjE)+
+apply (rule conjI)
+apply (rule permute_eq_iff[of "- p", THEN iffD1])
+apply (simp add: eqvts)
+apply (rule conjI)
+apply (rule fresh_star_permute_iff[of "- p", THEN iffD1])
+apply (simp add: eqvts)
+apply (rule conjI)
+apply (simp add: permute_eqvt[symmetric])
+apply (rule permute_eq_iff[of "- p", THEN iffD1])
+apply (subst permute_eqvt)
+apply (simp add: eqvts)
+done
 
 lemma
   assumes a: "alpha_lam_raw' t1 t2"