diff -r fa2b4b7af755 -r 3c6f8a4074c4 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Jan 12 16:12:54 2010 +0100
+++ b/Quot/quotient_info.ML	Tue Jan 12 16:21:42 2010 +0100
@@ -65,9 +65,8 @@
 
 exception NotFound
 
-(*******************)
-(* data containers *)
-(*******************)
+
+(** data containers **)
 
 (* info about map- and rel-functions for a type *)
 type maps_info = {mapfun: string, relmap: string}