diff -r 569f0e286400 -r d003f9e00c29 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Thu Dec 10 01:48:39 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 02:46:08 2009 +0100
@@ -151,7 +151,7 @@
   "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"