diff -r 9fb315392493 -r 8732ff59068b Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Wed May 26 15:37:56 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