--- a/src/Pure/type.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/type.ML Tue Sep 20 08:21:49 2005 +0200
@@ -632,7 +632,7 @@
fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
fun merge_types (types1, types2) =
- NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
+ NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) =>
err_in_decls d (the_decl types1 d) (the_decl types2 d);
end;