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

[Makarius]

*** 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


 	Makarius