changeset 50768 | 2172f82de515 |
parent 45444 | ac069060e08a |
child 52622 | e0ff1625e96d |
--- a/src/Tools/adhoc_overloading.ML Tue Jan 08 10:34:19 2013 +0100 +++ b/src/Tools/adhoc_overloading.ML Tue Jan 08 12:39:39 2013 +0100 @@ -53,7 +53,7 @@ fun merge ({internalize = int1, externalize = ext1}, {internalize = int2, externalize = ext2}) : T = - {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2), + {internalize = Symtab.merge_list (op =) (int1, int2), externalize = Symtab.join merge_ext (ext1, ext2)}; );