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) =