diff -r 87894b5156f4 -r 8557af71724e Nominal/Term5.thy
--- a/Nominal/Term5.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -173,10 +173,13 @@
 done
 
 lemma lets_ok3:
-  "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
-   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+  assumes a: "distinct [x, y]"
+  shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+         (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (subst alpha5_INJ)
 apply (rule conjI)
+apply (simp add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp only: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)