# HG changeset patch
# User wenzelm
# Date 1530824881 -7200
# Node ID f3c3c1e6133a36f320f13a05b245c56d0560392a
# Parent  9258f16d68b411c7acd03681c7c0827d9eaef2a3
store immutable result: fewer refs, mutexes, condvars;

diff -r 9258f16d68b4 -r f3c3c1e6133a src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Jul 04 22:44:24 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jul 05 23:08:01 2018 +0200
@@ -100,9 +100,9 @@
                     (*semantic race: some other threads might see the same
                       interrupt, until there is a fresh start*)
                     val _ =
-                      if Exn.is_interrupt_exn res then
-                        Synchronized.change var (fn _ => Expr (name, e))
-                      else ();
+                      if Exn.is_interrupt_exn res
+                      then Synchronized.change var (fn _ => Expr (name, e))
+                      else Synchronized.change var (fn _ => Result (Future.value_result res));
                   in res end
               | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
             end) ());