--- a/Nominal/Nominal2_Base.thy	Tue Jan 18 18:04:40 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 19:27:30 2011 +0100
@@ -1601,6 +1601,16 @@
   shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
 by (auto simp add: fresh_star_def fresh_def)
 
+lemma fresh_star_perm_set_conv:
+  fixes p::"perm"
+  assumes fresh: "as \<sharp>* p"
+  and     fin: "finite as"
+  shows "supp p \<sharp>* as"
+apply(rule fresh_star_supp_conv)
+apply(simp add: supp_finite_atom_set fin fresh)
+done
+
+
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
   by (auto simp add: fresh_star_def fresh_Pair)