--- a/Nominal-General/Nominal2_Base.thy	Fri Oct 01 07:11:47 2010 -0400
+++ b/Nominal-General/Nominal2_Base.thy	Mon Oct 04 07:25:37 2010 +0100
@@ -1247,6 +1247,10 @@
 where 
   "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
 
+lemma fresh_star_supp_conv:
+  shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
+by (auto simp add: fresh_star_def fresh_def)
+
 lemma fresh_star_prod:
   fixes as::"atom set"
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
@@ -1482,9 +1486,8 @@
 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)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def)
 done
 
 lemma at_set_avoiding2_atom: