--- a/Nominal/Nominal2_FSet.thy	Mon Jun 28 16:22:28 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Tue Jun 29 18:00:59 2010 +0100
@@ -67,7 +67,7 @@
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
 
-lemma fset_to_set_eqvt[eqvt]: 
+lemma fset_to_set_eqvt [eqvt]: 
   shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)"
   by (lifting set_eqvt)
 
@@ -77,10 +77,8 @@
 
 lemma supp_fset_to_set:
   shows "supp (fset_to_set S) = supp S"
-  apply (simp add: supp_def)
-  apply (simp add: eqvts)
-  apply (simp add: fset_cong)
-  done
+  unfolding supp_def
+  by (perm_simp) (simp add: fset_cong)
 
 lemma supp_finsert:
   fixes x::"'a::fs"