--- a/Nominal/Nominal2_FSet.thy	Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Mon Mar 29 00:30:47 2010 +0200
@@ -3,7 +3,7 @@
 begin
 
 lemma permute_rsp_fset[quot_respect]:
-  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
+  "(op = ===> list_eq ===> list_eq) permute permute"
   apply (simp add: eqvts[symmetric])
   apply clarify
   apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
@@ -44,7 +44,7 @@
 
 end
 
-lemma permute_fset[simp,eqvt]:
+lemma permute_fset[eqvt]:
   "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
   "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
   by (lifting permute_list.simps)