--- a/Nominal/Nominal2_FSet.thy	Mon Mar 22 09:02:30 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Mon Mar 22 10:15:46 2010 +0100
@@ -147,10 +147,22 @@
   apply (simp add: supp_fset_to_set)
   done
 
+lemma supp_fempty:
+  "supp {||} = {}"
+  by (simp add: supp_def eqvts)
+
 instance fset :: (at) fs
   apply (default)
   apply (induct_tac x rule: fset_induct)
-  apply (simp add: supp_def eqvts)
+  apply (simp add: supp_fempty)
+  apply (simp add: supp_at_finsert)
+  apply (simp add: supp_at_base)
+  done
+
+lemma supp_at_fset:
+  "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)"
+  apply (induct fset)
+  apply (simp add: supp_fempty)
   apply (simp add: supp_at_finsert)
   apply (simp add: supp_at_base)
   done