# HG changeset patch
# User haftmann
# Date 1603366639 0
# Node ID ff181cd78bb726f0db90a03907911accd163dbc9
# Parent  70b420065a07cb108bf9cdf35159d064a701f8cb
enforce strict nesting of local theories

diff -r 70b420065a07 -r ff181cd78bb7 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Oct 22 08:39:08 2020 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Oct 22 11:37:19 2020 +0000
@@ -361,7 +361,7 @@
 
 val exit_of = #exit o bottom_of;
 
-fun exit lthy = exit_of lthy lthy;
+fun exit lthy = exit_of lthy (assert_bottom lthy);
 val exit_global = Proof_Context.theory_of o exit;
 
 fun exit_result decl (x, lthy) =
diff -r 70b420065a07 -r ff181cd78bb7 src/Pure/Isar/target_context.ML
--- a/src/Pure/Isar/target_context.ML	Thu Oct 22 08:39:08 2020 +0200
+++ b/src/Pure/Isar/target_context.ML	Thu Oct 22 11:37:19 2020 +0000
@@ -21,7 +21,7 @@
 fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
   | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
 
-val end_named_cmd = Local_Theory.assert_bottom #> Local_Theory.exit_global;
+val end_named_cmd = Local_Theory.exit_global;
 
 fun switch_named_cmd NONE (Context.Theory thy) =
       (Context.Theory o end_named_cmd, Named_Target.theory_init thy)