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

[Makarius]

On Tue, 13 Aug 2013, Andreas Lochbihler wrote:

> 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.

This should work in Isabelle/ef65d5ee60cf.  Are there any remaining 
problems in the concrete application behind the example?


 	Makarius