--- a/Nominal/Nominal2_FSet.thy	Fri Sep 03 22:35:35 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Sep 04 05:43:03 2010 +0800
@@ -36,14 +36,12 @@
 
 end
 
-lemma permute_fset[simp]:
+lemma permute_fset[simp, eqvt]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
   and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-declare permute_fset[eqvt]
-
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -113,7 +111,7 @@
   apply (simp add: fresh_set_empty)
   apply simp
   apply (unfold fresh_def)
-  apply (simp add: supp_atom_insert)
+  apply (simp add: supp_of_fin_insert)
   apply (rule conjI)
   apply (unfold fresh_star_def)
   apply simp