diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Wed Jan 13 00:46:31 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Jan 13 09:19:20 2010 +0100
@@ -218,7 +218,7 @@
   val warns = map_check_aux rty []
 in
   if null warns then () 
-  else warning ("No map function defined for " ^ (commas warns) ^ 
+  else warning ("No map function defined for " ^ commas warns ^
                 ". This will cause problems later on.")
 end
 
@@ -227,16 +227,16 @@
 (*** interface and syntax setup ***)
 
 
-(* the ML-interface takes a list of 5-tuples consisting of 
-                                                         
-    - the name of the quotient type                       
-    - its free type variables (first argument)            
-    - its mixfix annotation                               
-    - the type to be quotient                             
-    - the relation according to which the type is quotient  
-                                                        
-   it opens a proof-state in which one has to show that the
-   relations are equivalence relations                      
+(* the ML-interface takes a list of 5-tuples consisting of:
+
+ - the name of the quotient type
+ - its free type variables (first argument)
+ - its mixfix annotation
+ - the type to be quotient
+ - the relation according to which the type is quotient
+
+ it opens a proof-state in which one has to show that the
+ relations are equivalence relations
 *)
 
 fun quotient_type quot_list lthy =