--- a/Attic/Quot/quotient_info.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_info.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,11 +1,9 @@
-(*  Title:      quotient_info.thy
+(*  Title:      HOL/Tools/Quotient/quotient_info.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Data slots for the quotient package.
-
+Data slots for the quotient package.
 *)
 
-
 signature QUOTIENT_INFO =
 sig
   exception NotFound
@@ -61,7 +59,7 @@
   (type T = maps_info Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))
+   fun merge data = Symtab.merge (K true) data)
 
 fun maps_defined thy s =
   Symtab.defined (MapsData.get thy) s
@@ -125,7 +123,7 @@
   (type T = quotdata_info Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))
+   fun merge data = Symtab.merge (K true) data)
 
 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
   {qtyp = Morphism.typ phi qtyp,
@@ -195,7 +193,7 @@
 fun qconsts_lookup thy t =
   let
     val (name, qty) = dest_Const t
-    fun matches x =
+    fun matches (x: qconsts_info) =
       let
         val (name', qty') = dest_Const (#qconst x);
       in
@@ -284,10 +282,9 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
 
 val _ = map improper_command
-  [(print_mapsinfo, "print_maps", "prints out all map functions"),
+  [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
    (print_quotinfo, "print_quotients", "prints out all quotients"),
    (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
 
 
 end; (* structure *)
-