[isabelle-dev] including raises Attempt to perform non-trivial merge of theories

[Andreas Lochbihler]

Dear all,

in Isabelle abd760a19e22, I get the error "Attempt to perform non-trivial merge of 
theories" when I include a bundle from another theory and there are at least two imports.
In the attachment, there's an example.

Best,
Andreas
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Scratch.thy
Type: application/x-extension-thy
Size: 105 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130813/d5f3fa66/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ScratchA.thy
Type: application/x-extension-thy
Size: 123 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130813/d5f3fa66/attachment-0001.bin>