--- a/Nominal/Ex/Multi_Recs.thy	Mon Dec 05 15:34:12 2011 +0000
+++ b/Nominal/Ex/Multi_Recs.thy	Mon Dec 05 16:12:44 2011 +0000
@@ -49,51 +49,6 @@
 thm multi_recs.perm_bn_simps
 thm multi_recs.bn_finite
 
-
-lemma at_set_avoiding5:
-  assumes "finite xs"
-  and     "finite (supp c)"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
-using assms
-apply(erule_tac c="c" in at_set_avoiding)
-apply(auto)
-done
-
-lemma
-  fixes c::"'a::fs"
-  assumes a:  "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"
-  shows "y = LetRec lrbs exp \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp))")
-apply(erule exE)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(simp add: multi_recs.fv_bn_eqvt)
-using Abs_rename_set'
-apply -
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bs lrbs" in meta_spec)
-apply(drule_tac x="(lrbs, exp)" in meta_spec)
-apply(drule meta_mp)
-apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair)
-apply(drule meta_mp)
-apply(simp add: multi_recs.bn_finite)
-apply(erule exE)
-apply(erule conjE)
-apply(rotate_tac 6)
-apply(drule sym)
-apply(simp add: multi_recs.fv_bn_eqvt)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: multi_recs.eq_iff)
-apply(rule at_set_avoiding1)
-apply(simp add: multi_recs.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(rule finite_sets_supp)
-apply(simp add: multi_recs.bn_finite)
-done
-
 end