--- a/Nominal/Nominal2_Supp.thy	Wed Mar 24 13:54:20 2010 +0100
+++ b/Nominal/Nominal2_Supp.thy	Wed Mar 24 14:49:51 2010 +0100
@@ -483,4 +483,19 @@
 apply(auto simp add: fresh_star_def fresh_def)
 done
 
+lemma at_set_avoiding2_atom:
+  assumes "finite (supp c)" "finite (supp x)"
+  and     b: "xa \<sharp> x"
+  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
+proof -
+  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
+  have c: "(p \<bullet> xa) \<sharp> c" using p1
+    unfolding fresh_star_def Ball_def 
+    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
+  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+  then show ?thesis by blast
+qed
+
 end