diff -r 6504ea98623c -r 35a8e15b7e03 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Nov 04 16:56:16 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 04 20:10:23 2019 +0100
@@ -294,7 +294,9 @@
       let
         val State ((node', pr_ctxt), _) =
           node |> apply
-            (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
+            (fn _ =>
+              node_presentation
+                (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
             (K ());
       in State ((Toplevel, pr_ctxt), get_theory node') end
   | (Keep f, node) =>