changeset 17496 | 26535df536ae |
parent 17412 | e26cb20ef0cc |
child 17587 | 760c6ade4ab6 |
--- a/src/Pure/Isar/method.ML Tue Sep 20 08:20:22 2005 +0200 +++ b/src/Pure/Isar/method.ML Tue Sep 20 08:21:49 2005 +0200 @@ -541,7 +541,7 @@ val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups => + fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups => error ("Attempt to merge different versions of method(s) " ^ commas_quote dups); fun print _ meths =