Hi Makarius, > On 14 Mar 2020, at 22:25, Makarius <[email protected]> wrote: > > 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.
Great, thanks! Your change allowed me to remove a workaround of an additional Thm.transfer in lift_bnf (c.f. isabelle/1cf958713cf7). I pushed this to the post-release dev-repository. I don't think that this changes anything observable for users. So it is probably fine if the release still includes the workaround. Dmitriy _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
