[isabelle-dev] NEWS: Local_Theory.restore versus Local_Theory.reset

[Dmitriy Traytel]

> On 05 Mar 2016, at 23:11, Makarius <makarius at sketis.net> wrote:
> 
> *** ML ***
> 
> * Local_Theory.restore has been renamed to Local_Theory.reset to
> emphasize its disruptive impact on the cumulative context, notably the
> scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
> only appropriate when targets are managed, e.g. starting from a global
> theory and returning to it. Regular definitional packages should use
> balanced blocks of Local_Theory.open_target versus
> Local_Theory.close_target instead. Rare INCOMPATIBILITY.
> 
> 
> This refers to Isabelle/aae510e9a698. This changeset also shows that remaining uses of the disruptive Local_Theory.reset are here:
> 
> src/HOL/Library/bnf_axiomatization.ML
> src/HOL/Tools/Lifting/lifting_def.ML
> src/HOL/Tools/Lifting/lifting_def_code_dt.ML
> src/HOL/Tools/Transfer/transfer_bnf.ML

The uses in

src/HOL/Library/bnf_axiomatization.ML
src/HOL/Tools/Transfer/transfer_bnf.ML

are gone in b5d656bf0441. The one in transfer_bnf.ML actually became obsolete with change eeaa2f7b5329 (or some of its immediate predecessors)—I somehow didn’t think of removing it.

Dmitriy