diff -r 491dde407f40 -r 5d06e1dba69a quotient.ML
--- a/quotient.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -39,8 +39,8 @@
 end
 
 
-(* definition of the quotient type *)
-(***********************************)
+(* definition of quotient types *)
+(********************************)
 
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =