Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;
authorwenzelm
Fri, 04 Sep 2015 11:38:35 +0200
changeset 61111 2618e7e3b5ea
parent 61110 6b7c2ecc6aea
child 61112 e966c311e9a7
proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;
src/Pure/Isar/local_theory.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle