--- a/quotient_info.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -45,7 +45,6 @@
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
-(* FIXME: this should be done using a generic context *)
 
 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
   (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
@@ -72,7 +71,7 @@
            "declaration of map information"))
 
 
-(* info about the quotient types *)
+(* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
 structure QuotData = Theory_Data
@@ -117,7 +116,7 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
-(* environments of quotient and raw types *)
+(* FIXME: obsolete: environments for quotient and raw types *)
 type qenv = (typ * typ) list
 
 fun mk_qenv ctxt =