tuned;

--- a/src/Pure/Isar/toplevel.ML	Thu Dec 29 12:27:55 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 29 12:34:40 2022 +0100
@@ -313,9 +313,10 @@
   | (Transaction (f, g), node) => update (fn x => f int x) g node
   | _ => raise UNDEF);
 
-fun apply_union _ [] _ = raise UNDEF
-  | apply_union int (tr :: trs) state =
-      apply_union int trs state
+fun apply_body _ [] _ = raise UNDEF
+  | apply_body int [tr] state = apply_tr int tr state
+  | apply_body int (tr :: trs) state =
+      apply_body int trs state
         handle Runtime.UNDEF => apply_tr int tr state;
 
 fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) =
@@ -328,7 +329,7 @@
 in
 
 fun apply_capture int name markers trans state =
-  (apply_union int trans state |> apply_markers name markers)
+  (apply_body int trans state |> apply_markers name markers)
     handle exn => (state, SOME exn);
 
 end;