--- a/Nominal/Nominal2_FSet.thy	Tue May 25 10:43:19 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Tue May 25 17:01:37 2010 +0200
@@ -103,5 +103,20 @@
   apply (simp add: supp_at_base)
   done
 
+lemma fresh_star_atom:
+  "fset_to_set s \<sharp>* (a :: _ :: at_base) \<Longrightarrow> atom a \<sharp> fset_to_set s"
+  apply (induct s)
+  apply (simp add: fresh_set_empty)
+  apply simp
+  apply (unfold fresh_def)
+  apply (simp add: supp_atom_insert)
+  apply (rule conjI)
+  apply (unfold fresh_star_def)
+  apply simp
+  apply (unfold fresh_def)
+  apply (simp add: supp_at_base supp_atom)
+  apply clarify
+  apply auto
+  done
 
 end