src/Pure/Isar/toplevel.ML

         State (node_presentation (Theory (Context.Theory (f ()))), NONE)) ()
   | (Exit, node as Theory (Context.Theory thy)) =>
       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) =>
       Runtime.controlled_execution (try generic_theory_of state)
         (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()