--- a/src/Tools/adhoc_overloading.ML Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Tools/adhoc_overloading.ML Sat Jan 08 17:14:48 2011 +0100
@@ -53,10 +53,11 @@
if ext_name1 = ext_name2 then ext_name1
else duplicate_variant_err int_name ext_name1;
- fun merge ({internalize=int1, externalize=ext1},
- {internalize=int2, externalize=ext2}) =
- {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
- externalize=Symtab.join merge_ext (ext1, ext2)};
+ fun merge
+ ({internalize = int1, externalize = ext1},
+ {internalize = int2, externalize = ext2}) : T =
+ {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2),
+ externalize = Symtab.join merge_ext (ext1, ext2)};
);
fun map_tables f g =