author | wenzelm |
Sun, 02 May 2021 15:22:19 +0200 | |
changeset 73614 | 14757eb3b249 |
parent 73613 | c1d8cd6d1a49 |
child 73615 | e768759ce6c5 |
--- a/src/Pure/Isar/toplevel.ML Sun May 02 14:07:19 2021 +0200 +++ b/src/Pure/Isar/toplevel.ML Sun May 02 15:22:19 2021 +0200 @@ -634,7 +634,7 @@ val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); - val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ())); + val _ = get_hooks () |> List.app (fn f => ignore \<^try>\<open>f tr st st'\<close>); in (st', opt_err') end; end;