src/Pure/Isar/toplevel.ML

   | (Keep f, node) => no_update (fn x => f int x) node state
   | (Transaction _, Toplevel) => raise UNDEF
   | (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)) =
   let
     val state' =

   in (state', NONE) end;
 
 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;