--- a/src/Pure/Concurrent/future.ML Tue Aug 04 09:33:05 2020 +0000
+++ b/src/Pure/Concurrent/future.ML Wed Aug 05 12:34:23 2020 +0200
@@ -27,7 +27,6 @@
val default_params: params
val forks: params -> (unit -> 'a) list -> 'a future list
val fork: (unit -> 'a) -> 'a future
- val get_finished: 'a future -> 'a
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
@@ -508,8 +507,6 @@
| exns => Exn.Exn (Par_Exn.make exns))
else res);
-fun get_finished x = Exn.release (get_result x);
-
local
fun join_next atts deps = (*requires SYNCHRONIZED*)