--- a/Nominal/Ex/Lambda.thy	Tue Dec 20 18:07:48 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Dec 21 13:06:09 2011 +0900
@@ -277,7 +277,7 @@
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
-  apply(auto simp add: lam.distinct lam.eq_iff)
+  apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
   apply(blast)+
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
@@ -402,7 +402,7 @@
 proof -
   obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh)
   have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs
-    by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
+    by (auto simp add: Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
   also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)
   also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric])
   finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp