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

[Makarius]

Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
versus old uses of Local_Theory.restore.

Local_Theory.open_target is the internal version of "context begin", where 
Local_Theory.close_target is "end".  The ML signature is now a bit more 
concise form than before.  It has already been used successfully in 
Eisbach, to lay out a local situation for the internal construction.


Here is a quick example that shows how to get polymorphic constants out of 
local theory specifications, with such official context nesting:

context fixes x :: 'a
begin

declare [[show_types]]
ML_val ‹
   val lthy = @{context};
   val (_, lthy1) = lthy |> Local_Theory.open_target;
   val ((t, (_, th)), lthy2) = lthy1
     |> Local_Theory.define ((@{binding c}, NoSyn), (Attrib.empty_binding, @{term "λy. x"}));
   val lthy3 = lthy2 |> Local_Theory.close_target;
   val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy3);

   val th' = th |> singleton (Proof_Context.export lthy2 lthy3);
   val th'' = th' |> singleton (Proof_Context.export lthy3 thy_ctxt);

   writeln (Display.string_of_thm lthy2 th);  (*monomorphic*)
   writeln (Display.string_of_thm lthy3 th');  (*partly polymorphic*)
   writeln (Display.string_of_thm thy_ctxt th'');  (*fully polymorphic*)
›

Thus the brute-force Local_Theory.restore is avoided, which only works 
properly at the boundary of local theory command transactions anyway.


Eliminating Local_Theory.restore is one of these continuous reform 
projects that can be done now or later.  Note that it would also achieve 
better results for "private datatype", because Local_Theory.restore 
disrupts the continuity of the naming policy.

It is up to the BNF guys to say if they intend to do something for the 
Isabelle2015 release, or just leave the status quo.  It is unlikely that 
anybody will notice fine points of private datatype definitions before the 
next release after Isabelle2015.


 	Makarius