--- a/Nominal/Nominal2_Base.thy	Sun Nov 28 16:37:34 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Nov 29 05:10:02 2010 +0000
@@ -1589,6 +1589,15 @@
   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
   unfolding fresh_star_def fresh_def by blast
 
+lemma at_set_avoiding1:
+  assumes "finite xs"
+  and     "finite (supp c)"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c"
+using assms
+apply(erule_tac c="c" in at_set_avoiding)
+apply(auto)
+done
+
 lemma at_set_avoiding2:
   assumes "finite xs"
   and     "finite (supp c)" "finite (supp x)"