tuned;
authorwenzelm
Sun, 02 May 2021 15:22:19 +0200
changeset 73614 14757eb3b249
parent 73613 c1d8cd6d1a49
child 73615 e768759ce6c5
tuned;
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;