# HG changeset patch
# User wenzelm
# Date 1596623663 -7200
# Node ID df99d26efeebeb84b8bdb615e111a91fe66dedde
# Parent  41393ecb57ace7ccd69e36f6a377678f50d4512a
unused;

diff -r 41393ecb57ac -r df99d26efeeb src/Pure/Concurrent/future.ML
--- 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*)