[isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore

[Makarius]

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