| changeset 78757 | a094bf81a496 |
| parent 78725 | 3c02ad5a1586 |
| child 78764 | a3dcae9a2ebe |
--- a/src/Pure/Isar/toplevel.ML Wed Oct 11 11:07:00 2023 +0200 +++ b/src/Pure/Isar/toplevel.ML Wed Oct 11 11:27:01 2023 +0200 @@ -331,7 +331,7 @@ in fun apply_capture int name markers trans state = - (case Exn.capture (fn () => apply_body int trans state |> apply_markers name markers) () of + (case Exn.capture_body (fn () => apply_body int trans state |> apply_markers name markers) of Exn.Res res => res | Exn.Exn exn => (state, SOME exn));