# HG changeset patch
# User wenzelm
# Date 1619961739 -7200
# Node ID 14757eb3b24980b213f3e1d44f130769a71114fe
# Parent  c1d8cd6d1a49d347fd4eb91f195d9b30c01455f7
tuned;

diff -r c1d8cd6d1a49 -r 14757eb3b249 src/Pure/Isar/toplevel.ML
--- 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;