# HG changeset patch
# User wenzelm
# Date 1672313680 -3600
# Node ID 9e09030737e53ff975570bffdaae2518eab0d941
# Parent  56d76e8cecf407119ee39aeedd6f50bb7ac10b8f
tuned;

diff -r 56d76e8cecf4 -r 9e09030737e5 src/Pure/Isar/toplevel.ML
--- 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;