src/Pure/Isar/method.ML
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 =