[isabelle-dev] CONTEXT exception after locale interpretation with setup_lifting

[Makarius]

On 28/02/2020 17:44, Traytel Dmitriy wrote:
> 
> I found the following interaction of setup_lifting and locale interpretations
> surprising. In the below example, the first two local_setup's succeed, whereas
> the third one fails with a CONTEXT exception in Isabelle/b94053ca8d77. And
> this failure occurs despite the fact that Lifting_Info.lookup_quotients
> already invokes Morphism.transfer_morphism. All three local_setup's work in
> Isabelle2019. If I were to guess, I believe this has to do with the
> commit c82f59c47aaf, which changes the meaning of Morphism.transfer_morphism.
> But I have to admit that I don't understand the Context.subthy_id check in the
> Thm.join_transfer function that is introduced there.

Bisection yields the following result:

changeset:   70472:9179e7a98196
user:        wenzelm
date:        Tue Aug 06 17:26:40 2019 +0200
files:       src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Transfer/transfer.ML
description:
clarified signature;
more careful treatment of implicit context;

The problem is in Thm.join_transfer from here:
changeset:   70310:c82f59c47aaf
user:        wenzelm
date:        Mon Jun 03 20:09:43 2019 +0200
files:       src/Pure/morphism.ML src/Pure/thm.ML
description:
clarified transfer_morphism: implicit join_certificate, e.g. relevant for
complex cascades of morphisms such as class locale interpretation;

I have now amended that here:
changeset:   71553:cf2406e654cf
tag:         tip
user:        wenzelm
date:        Sat Mar 14 21:58:29 2020 +0100
files:       src/Pure/thm.ML
description:
more robust: proper transfer if Context.eq_thy_id;


Thus it also fits better to Thm.join_transfer_context.


	Makarius