src/Pure/sign.ML
changeset 45632 b23c42b9f78a
parent 45427 fca432074fb2
child 47005 421760a1efe7
equal deleted inserted replaced
45631:6bdf8b926f50 45632:b23c42b9f78a
   147       val ctxt = Syntax.init_pretty pp;
   147       val ctxt = Syntax.init_pretty pp;
   148       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   148       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   149       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   149       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   150 
   150 
   151       val naming = Name_Space.default_naming;
   151       val naming = Name_Space.default_naming;
   152       val syn = Syntax.merge_syntaxes syn1 syn2;
   152       val syn = Syntax.merge_syntax (syn1, syn2);
   153       val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
   153       val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
   154       val consts = Consts.merge (consts1, consts2);
   154       val consts = Consts.merge (consts1, consts2);
   155     in make_sign (naming, syn, tsig, consts) end;
   155     in make_sign (naming, syn, tsig, consts) end;
   156 );
   156 );
   157 
   157