On Sun, 12 Apr 2015, Florian Haftmann wrote:
I have done a grep on this:
src/Pure/Isar/named_target.ML:197: (Context.Proof o Local_Theory.restore,
lthy)
This is the only place where Local_Theory.restore is used according to its
original idea. It might be possible to get rid of it eventually, like the
old "reinit", but it is not a big deal.
src/HOL/Library/bnf_axiomatization.ML:84: ||> `Local_Theory.restore;
src/HOL/Tools/BNF/bnf_def.ML:794: ? Local_Theory.restore;
...
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML:633: ||> `Local_Theory.restore;
That is all about BNF, and Dmitriy has already said that he will continue
work there after the relase. Eliminating Local_Theory.restore will make
it possible to use "private datatype" for example, and get the expected
effect on the name space entries.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
