src/Pure/sign.ML
changeset 45632 b23c42b9f78a
parent 45427 fca432074fb2
child 47005 421760a1efe7
     1.1 --- a/src/Pure/sign.ML	Fri Nov 25 14:23:36 2011 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Nov 25 16:32:29 2011 +0100
     1.3 @@ -149,7 +149,7 @@
     1.4        val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
     1.5  
     1.6        val naming = Name_Space.default_naming;
     1.7 -      val syn = Syntax.merge_syntaxes syn1 syn2;
     1.8 +      val syn = Syntax.merge_syntax (syn1, syn2);
     1.9        val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
    1.10        val consts = Consts.merge (consts1, consts2);
    1.11      in make_sign (naming, syn, tsig, consts) end;