> On 05 Mar 2016, at 23:11, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev