equal
deleted
inserted
replaced
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 |