diff -r b91782991dc8 -r 95ee248b3832 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Jan 21 11:11:22 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 21 12:03:47 2010 +0100
@@ -101,7 +101,7 @@
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp bexeq_rsp
+lemmas [quot_respect] = quot_rel_rsp
 lemmas [quot_equiv] = identity_equivp
 
 (* Lemmas about simplifying id's. *)