src/Pure/sign.ML
changeset 17496 26535df536ae
parent 17412 e26cb20ef0cc
child 17995 8b9c6af78a67
--- a/src/Pure/sign.ML	Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/sign.ML	Tue Sep 20 08:21:49 2005 +0200
@@ -227,7 +227,7 @@
       val naming = NameSpace.default_naming;
       val syn = Syntax.merge_syntaxes syn1 syn2;
       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
-      val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
+      val consts = NameSpace.merge_tables (eq_snd (op =)) (consts1, consts2)
         handle Symtab.DUPS cs => err_dup_consts cs;
       val constraints = Symtab.merge (op =) (constraints1, constraints2)
         handle Symtab.DUPS cs => err_inconsistent_constraints cs;