# HG changeset patch
# User haftmann
# Date 1501827177 -7200
# Node ID 13e7dc5f7c3d761291c12d55effa16298393ec40
# Parent  a849ce33923d791568d386441ce66860acbe81d6
exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements

diff -r a849ce33923d -r 13e7dc5f7c3d src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Aug 04 08:12:54 2017 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Aug 04 08:12:57 2017 +0200
@@ -217,8 +217,8 @@
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.init_target
-      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close,
-       exit = Local_Theory.exit_of lthy} (Local_Theory.operations_of lthy)
+      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close}
+      (Local_Theory.operations_of lthy)
   end;
 
 in
diff -r a849ce33923d -r 13e7dc5f7c3d src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Aug 04 08:12:54 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 04 08:12:57 2017 +0200
@@ -67,14 +67,12 @@
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} ->
     operations -> Proof.context -> local_theory
-  val exit_of: local_theory -> local_theory -> Proof.context
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory,
-    exit: local_theory -> Proof.context} -> operations ->
-    local_theory -> Binding.scope * local_theory
+  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} ->
+    operations -> local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> Binding.scope * local_theory
   val close_target: local_theory -> local_theory
 end;
@@ -356,7 +354,7 @@
     (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)]
       | _ => error "Local theory already initialized");
 
-val exit_of = #exit o top_of;
+val exit_of = #exit o bottom_of;
 
 fun exit lthy = exit_of lthy lthy;
 val exit_global = Proof_Context.theory_of o exit;
@@ -377,19 +375,19 @@
 
 (* nested targets *)
 
-fun init_target {background_naming, after_close, exit} operations lthy =
+fun init_target {background_naming, after_close} operations 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', exit, true, target)));
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close', exit_of lthy, true, target)));
   in (scope, lthy') end;
 
 fun open_target lthy =
-  init_target {background_naming = background_naming_of lthy, after_close = I,
-    exit = exit_of lthy} (operations_of lthy) lthy;
+  init_target {background_naming = background_naming_of lthy, after_close = I}
+    (operations_of lthy) lthy;
 
 fun close_target lthy =
   let