# HG changeset patch
# User wenzelm
# Date 1333402044 -7200
# Node ID d6c76b1823fb2c02f0bfdbe6c354cde4d192dd32
# Parent  d2367cc84235dad877f70e942773ab3248be88b5
better restore after close_target;

diff -r d2367cc84235 -r d6c76b1823fb src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Apr 02 21:52:03 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Apr 02 23:27:24 2012 +0200
@@ -128,7 +128,7 @@
   |> Data.map (cons (make_lthy (naming, operations, target)));
 
 fun close_target lthy =
-  assert_bottom false lthy |> Data.map tl;
+  assert_bottom false lthy |> Data.map tl |> restore;
 
 fun map_contexts f lthy =
   let val n = level lthy in