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