# HG changeset patch
# User wenzelm
# Date 1697019766 -7200
# Node ID 6ca807f7fed02560754d4abb5756c3c0303933c8
# Parent  461e924cc82526701c37c45be58c17680c9c6609
tuned;

diff -r 461e924cc825 -r 6ca807f7fed0 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Oct 11 11:59:24 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Oct 11 12:22:46 2023 +0200
@@ -498,12 +498,12 @@
 fun get_result x =
   (case peek x of
     NONE => Exn.Exn (Fail "Unfinished future")
-  | SOME res =>
-      if Exn.is_interrupt_exn res then
+  | SOME result =>
+      if Exn.is_interrupt_exn result then
         (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
-          [] => res
+          [] => result
         | exns => Exn.Exn (Par_Exn.make exns))
-      else res);
+      else result);
 
 local