diff -r 16e6140225af -r da59c94bed7e Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Apr 03 23:09:13 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Apr 04 06:19:38 2012 +0100
@@ -629,6 +629,7 @@
   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  by (simp add: set_eqvt[symmetric])
 
 instance 
 proof