diff -r 78721f3adb13 -r 62eaaffe6e47 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Apr 28 11:09:19 2010 +0200
+++ b/src/Pure/sign.ML	Wed Apr 28 11:13:11 2010 +0200
@@ -155,7 +155,7 @@
 
       val naming = Name_Space.default_naming;
       val syn = Syntax.merge_syntaxes syn1 syn2;
-      val tsig = Type.merge_tsigs pp (tsig1, tsig2);
+      val tsig = Type.merge_tsig pp (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
     in make_sign (naming, syn, tsig, consts) end;
 );