--- a/Nominal/Nominal2_Supp.thy	Sat Mar 20 13:50:00 2010 +0100
+++ b/Nominal/Nominal2_Supp.thy	Sat Mar 20 16:27:51 2010 +0100
@@ -466,6 +466,21 @@
   then show "p \<bullet> x = x" using eq by simp
 qed
 
+section {* at_set_avoiding2 *}
 
+lemma at_set_avoiding2
+  assumes "finite xs"
+  and     "finite (supp c)" "finite (supp x)"
+  and     "xs \<sharp>* x"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+apply(auto simp add: fresh_star_def fresh_def)
+done
 
 end
\ No newline at end of file