--- 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