--- 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) ());