# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269677709 -3600
# Node ID 7eb95f86f87f59b1239ef6f99a9cb33a903fd3d9
# Parent  e8cf0520c82030bca9a8739e5568cc849d1f9f76
Minor fix.

diff -r e8cf0520c820 -r 7eb95f86f87f Nominal/ExLetRec.thy
--- 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: