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

[Ondřej Kunčar]

On 08/13/2013 04:19 PM, Andreas Lochbihler wrote:
> 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.

The problem happens in the function 
Transfer.abstract_equalities_transfer where the theorem that is supposed 
to be registered by the attribute [transfer_rule] is combined with other 
theorems (used for preprocessing) that are stored in the theory data of 
the Transfer package (they are retrieved through Transfer.get_relator_eq).

Now, I suppose that the theorem that is being registered by 
[transfer_rule] always lives in the theory where the attribute is 
applied and thus the other theorems used for preprocessing don't have to 
be explicitly transferred to a higher theory. This is true, for example, 
when declare foo[transfer_rule] is used.

But apparently it is not true for bundles. It seems that theorems that 
are stored in a bundle still live in a theory where the bundle was 
defined, and not in the theory where the attributes are applied (i.e., 
where including is invoked). Shouldn't be the theorems that are stored 
in a bundle transferred to a theory where including is invoked before 
the attributes are applied to them?

Ondrej