--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:06:13 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:51:38 2010 +0100
@@ -272,7 +272,7 @@
 
 lemma quotient_compose_list_gen:
   assumes a: "Quotient r2 abs2 rep2"
-  and     b: "equivp r2" (* reflp should be enough... *)
+  and     b: "equivp r2" (* reflp is not enough *)
   shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2))
                (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
   unfolding Quotient_def comp_def