# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273511340 -3600
# Node ID e417be53916e2bb69815258a4d70e964c13ed120
# Parent  705dc7532ee34b1e42a4fc0799c48b78d88ce314
fixed a problem with non-existant alphas2

diff -r 705dc7532ee3 -r e417be53916e Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Mon May 10 17:57:22 2010 +0100
+++ b/Nominal/Ex/ExLetRec.thy	Mon May 10 18:09:00 2010 +0100
@@ -43,13 +43,14 @@
 
 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))"
-  by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base)
+  apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
+  done
 
 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: alphas2 fresh_star_def eqvts supp_at_base)
+  apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
   done
 
 lemma lets_ok3: