# HG changeset patch
# User wenzelm
# Date 1266613612 -3600
# Node ID 3aea183d05dbf3727f2de5b126c1899534aa28db
# Parent  663436ed5bd68abcb4479e94193bdadcba592e74
made SML/NJ happy;

diff -r 663436ed5bd6 -r 3aea183d05db src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Feb 19 22:06:01 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Feb 19 22:06:52 2010 +0100
@@ -59,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
@@ -123,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,
@@ -193,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