--- a/Nominal/FSet.thy	Wed Jun 16 14:26:23 2010 +0200
+++ b/Nominal/FSet.thy	Wed Jun 16 22:29:42 2010 +0100
@@ -163,6 +163,7 @@
 
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
+  apply(simp del: list_eq.simps)
   by auto
 
 lemma append_rsp_unfolded: