--- a/Nominal/Ex/Lambda.thy	Tue Feb 01 08:57:50 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Feb 01 09:07:55 2011 +0900
@@ -140,7 +140,7 @@
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
 apply(simp add: fresh_star_def)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
+apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
 apply(subst (asm) Abs_eq_iff2)
 apply(simp add: alphas atom_eqvt)
 apply(clarify)
@@ -168,9 +168,6 @@
 apply(auto simp add: fresh_star_def fresh_Pair)[1]
 apply(rule perm_supp_eq)
 apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule conjI)
-apply(simp add: Abs_fresh_iff)
-apply(drule sym)
 apply(simp add: Abs_fresh_iff)
 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def