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