tuned;

--- a/src/Pure/Isar/toplevel.ML	Wed Dec 28 22:37:46 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 29 11:49:11 2022 +0100
@@ -282,7 +282,15 @@
 fun apply_presentation g (st as State (node, (prev_thy, _))) =
   State (node, (prev_thy, g st));
 
-fun apply f g node =
+fun no_update f node state =
+  Runtime.controlled_execution (try generic_theory_of state)
+    (fn () =>
+      let
+        val prev_thy = previous_theory_of state;
+        val state' = State (node_presentation node, (prev_thy, NONE));
+      in apply_presentation f state' end) ()
+
+fun update f g node =
   let
     val node_pr = node_presentation node;
     val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
@@ -305,21 +313,15 @@
   | (Exit, node as Theory (Context.Theory thy)) =>
       let
         val State ((node', pr_ctxt), _) =
-          node |> apply
+          node |> update
             (fn _ =>
               node_presentation
                 (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
             no_presentation;
       in State ((Toplevel, pr_ctxt), (get_theory node', NONE)) end
-  | (Keep f, node) =>
-      Runtime.controlled_execution (try generic_theory_of state)
-        (fn () =>
-          let
-            val prev_thy = previous_theory_of state;
-            val state' = State (node_presentation node, (prev_thy, NONE));
-          in apply_presentation (fn st => f int st) state' end) ()
+  | (Keep f, node) => no_update (fn x => f int x) node state
   | (Transaction _, Toplevel) => raise UNDEF
-  | (Transaction (f, g), node) => apply (fn x => f int x) g node
+  | (Transaction (f, g), node) => update (fn x => f int x) g node
   | _ => raise UNDEF);
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)