# HG changeset patch
# User wenzelm
# Date 1441359515 -7200
# Node ID 2618e7e3b5ea69e69a1421c640741fa0ab3f7ae3
# Parent  6b7c2ecc6aea75d4cc020131952622c62137aa4f
proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;

diff -r 6b7c2ecc6aea -r 2618e7e3b5ea src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Sep 03 21:50:39 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Sep 04 11:38:35 2015 +0200
@@ -368,10 +368,11 @@
 fun init_target background_naming operations after_close lthy =
   let
     val _ = assert lthy;
+    val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
     val lthy' =
       target
-      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target)));
   in (scope, lthy') end;
 
 fun open_target lthy =