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

[Makarius]

On Mon, 19 Aug 2013, Makarius wrote:

> After two rounds of looking through it, I've devised the included change. It 
> seems to address the situation exposed by Andreas, but breaks 
> HOL/Quotient_Examples.thy here:
>
> lift_definition fmember :: "'a ⇒ 'a fset ⇒ bool" (infix "|∈|" 50) is "λx 
> xs. x ∈ set xs"
>   parametric member_transfer by simp
>
> exception THM 0 raised (line 404 of "thm.ML"):
>  transfer: not a super theory
>  bi_unique A  [bi_unique A]
>
>
> This might be either a problem with "the context" on your side, or something 
> else wrong in the system infrastructure.

After some delays I am back to this.  There was indeed a trivial incident 
with "the context":

changeset:   53203:8d41170242cb
user:        wenzelm
date:        Mon Aug 26 15:45:51 2013 +0200
files:       src/HOL/Tools/Lifting/lifting_def.ML
description:
proper context;


After that comes the actual change to transfer deep down in the system 
whenever attributed theorems are evaluated:

changeset:   53204:5d2fe75c6306
user:        wenzelm
date:        Mon Aug 26 15:57:09 2013 +0200
files:       src/Pure/more_thm.ML
description:
always transfer thm where attributes are applied -- relevant for internal 
'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. 
Proof_Context.retrieve_thms);


After that some unreleated thing I came across in your sources:

changeset:   53205:9745b7d4cc79
user:        wenzelm
date:        Mon Aug 26 16:13:20 2013 +0200
files:       src/HOL/Tools/Lifting/lifting_def.ML
description:
prefer Binding.name_of over Binding.print -- the latter leads to funny 
quotes and markup within the constructed term;


I can imagine how some old copy of Binding.str_of got somehow converted 
into the newer but wrong Binding.print.  Today this should never happen 
again, since the implementation manual (e.g. of Isabelle2013) says:

   \item @{ML Binding.print}~@{text "binding"} produces a string
   representation for human-readable output, together with some formal
   markup that might get used in GUI front-ends, for example.


 	Makarius