diff -r 385add25dedf -r 3ebc7ecfb0dd Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Nov 26 22:43:26 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Nov 27 22:55:29 2010 +0000
@@ -1583,9 +1583,15 @@
   assumes "finite xs"
   and     "finite (supp c)" "finite (supp x)"
   and     "xs \<sharp>* x"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> x = p \<bullet> x"
-using at_set_avoiding2[OF assms]
-by (auto simp add: supp_perm_eq)
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)"
+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(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def)
+done
 
 
 lemma at_set_avoiding2_atom: