--- a/Quot/QuotMain.thy	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 21 10:55:09 2010 +0100
@@ -100,8 +100,8 @@
 
 declare [[map "fun" = (fun_map, fun_rel)]]
 
-lemmas [quot_thm] = fun_quotient 
-lemmas [quot_respect] = quot_rel_rsp
+lemmas [quot_thm] = fun_quotient
+lemmas [quot_respect] = quot_rel_rsp bexeq_rsp
 lemmas [quot_equiv] = identity_equivp
 
 (* Lemmas about simplifying id's. *)