# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277830859 -3600
# Node ID b1549d391ea708cfacff326209d5a7ab3a113b9b
# Parent  1e0b3992189c11e937428c8a5c57a777ba361568
removed an "eqvt"-warning

diff -r 1e0b3992189c -r b1549d391ea7 Nominal/Nominal2_FSet.thy
--- 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"