diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Wed Jan 13 00:46:31 2010 +0100
+++ b/Quot/quotient_info.ML	Wed Jan 13 09:19:20 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}