Merging theories over different vocabulary

[Bart Bogaerts]

voc A{

...

}

voc B{

extern voc A

}

merge(TA,TB) might result in a theory over vocA. This should actually be a thoery over vocB, the largest of the two, even when they are equal. Now, this is depending on the order of the theories, which is unlogical

[Bart Bogaerts]

Whatever happens to this issue, the manual should be updated to clarify the invariants of this inference.

[Broes De Cat]

I don't really see the problem in this? When the resulting vocabulary already exists, it chooses that one (or one of those if there are multiple which are equal). If it does not already exist, a new one is created.

[Bart Bogaerts]

The problem is that you don't know over which vocabulary the result would be.

This resulted in problems in the MCS practicum where MX threw an error in case the result was over vocA, but not when it was over vocB.