--- a/Nominal/Ex/Let.thy	Mon Oct 04 12:39:57 2010 +0100
+++ b/Nominal/Ex/Let.thy	Tue Oct 05 07:30:37 2010 +0100
@@ -100,16 +100,9 @@
 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
-apply(subgoal_tac "-q \<bullet> (\<forall>assn trm. (set (bn assn) \<sharp>* c \<and>  y = Let assn trm) \<longrightarrow> P)")
-apply(perm_simp add: trm_assn.fv_bn_eqvt)
-(* HERE *)
-
-
-
 apply(simp add: set_eqvt)
 apply(subst (asm) tt)
 apply(rule_tac assms(4))
-apply(simp add: fresh_star_prod)
 apply(simp)
 apply(simp add: trm_assn.eq_iff)
 apply(drule supp_perm_eq[symmetric])