diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_typ.ML	Fri Jan 01 23:59:32 2010 +0100
@@ -218,8 +218,8 @@
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
 (*                                                          *)
-(* opens a proof-state in which one has to show that the    *)
-(* relation is an equivalence relation                      *)
+(* it opens a proof-state in which one has to show that the *)
+(* relations are equivalence relations                      *)
 
 fun quotient_type quot_list lthy = 
 let