tuned;
authorwenzelm
Wed, 11 Oct 2023 12:22:46 +0200
changeset 78760 6ca807f7fed0
parent 78759 461e924cc825
child 78761 6b3f13d39612
tuned;
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