On 22/01/2019 22:24, Florian Haftmann wrote:
> as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
> seen Local_Theory.reset invocations are gone, conveniently replaced by
> Local_Theory.subtarget_result.

This looks clean and canonical. At least we have Local_Theory.reset out
of the way in visible Isabelle/ML tool implementations: it is still
present inside Local_Theory.close_target, though.

I wonder what happens when that is removed: presumably it requires a lot
of fine-tuning to make everything work again without that hidden reset.


Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to