--- a/Nominal/ExLetRec.thy	Sat Mar 27 08:42:07 2010 +0100
+++ b/Nominal/ExLetRec.thy	Sat Mar 27 09:15:09 2010 +0100
@@ -35,14 +35,13 @@
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub)
-  done
+  by (simp add: trm_lts.eq_iff alphas2 set_sub)
 
 lemma lets_ok:
   "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
   apply (simp add: trm_lts.eq_iff)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alpha_gen2 fresh_star_def eqvts)
+  apply (simp_all add: alphas2 fresh_star_def eqvts)
   done
 
 lemma lets_ok3: