more robust: insist in finished future;

--- a/src/Pure/Concurrent/future.ML	Wed Aug 05 12:34:23 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 05 12:42:43 2020 +0200
@@ -27,6 +27,7 @@
   val default_params: params
   val forks: params -> (unit -> 'a) list -> 'a future list
   val fork: (unit -> 'a) -> 'a future
+  val get_result: 'a future -> 'a Exn.result
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list

--- a/src/Pure/Concurrent/lazy.ML	Wed Aug 05 12:34:23 2020 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Wed Aug 05 12:42:43 2020 +0200
@@ -103,7 +103,7 @@
                   let
                     val res0 = Exn.capture (restore_attributes e) ();
                     val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
-                    val res = Future.join_result x;
+                    val res = Future.get_result x;
                     val _ =
                       if not (Exn.is_interrupt_exn res) then
                         Synchronized.assign var (Result (Future.value_result res))