> thank you for the analysis. I have looked at this more closely now and, yes, > I believe this is the correct fix. Please go ahead and push.
See now http://isabelle.in.tum.de/reports/Isabelle/rev/e58623a33ba5 Florian > > Clemens > > > On 12 December, 2013 14:02 CET, Florian Haftmann > <[email protected]> wrote: > >> Hi Clemens, >> >> I have done an analysis, and it seems to me that the critical spot is >> >>> fun init name thy = >>> activate_all name thy Element.init (Morphism.transfer_morphism o >>> Context.theory_of) >>> (empty_idents, Context.Proof (Proof_Context.init_global thy)) >>> |-> Idents.put |> Context.proof_of; >> >> Using »empty_idents«, potentially pre-existing idents are chased away, >> whereas registrations are taken over from the initial background theory. >> >> This is no problem as long as >> a) no further registrations are added (as in »interpret«) >> b) the resulting target context is not used to setup further >> interpretations (which would not occur prior to Isabelle2013-1) >> >> I suggest to maintain the set of identifiers from the initial context, e.g. >> >>> fun init name thy = >>> let >>> val context = Context.Proof (Proof_Context.init_global thy); >>> val marked = Idents.get context; >>> val (marked', context') = activate_all name thy Element.init >>> (Morphism.transfer_morphism o Context.theory_of) (empty_idents, >>> context) >>> in >>> context' >>> |> Idents.put (merge_idents (marked, marked')) >>> |> Context.proof_of >>> end; >> >> I have glimpsed this pattern from roundup itself. >> >> I did an experimental plausibility check which exhibited no problems. >> The only point of manual intervention is in >> >> http://sourceforge.net/p/afp/code/ci/ecad5b18ca0edd5d3f3d257d56a1aff2b2ac0a1b/tree/thys/Launchbury/HSem.thy >> >> the »interpret subpcpo ?S by (rule subpcpo_fjc)«, which explicitly >> relied on re-interpretation of the fragment subpcpo_syn to obtain a >> particular specialized syntax; but this fragment is already shadowed by >> a global schematic interpretation »interpretation subpcpo_syn S for S.« in >> >> http://sourceforge.net/p/afp/code/ci/ecad5b18ca0edd5d3f3d257d56a1aff2b2ac0a1b/tree/thys/Launchbury/HOLCF-Set.thy >> >> (sorry for not giving direct links, but SF does not seem to support this). >> >> Touching such a fundamental thing, I would kindly ask for your opinion >> whether I should push this in that shape or you know about further >> issues which have to be taken care of. >> >> Thanks and all the best, >> Florian >> >> -- >> >> PGP available: >> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de >> > > > > > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
