diff -r 9b0daffc4054 -r bd9573735bdd src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Oct 01 12:00:00 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Oct 01 12:00:01 2008 +0200
@@ -40,7 +40,6 @@
   val fork_background: (unit -> 'a) -> 'a T
   val join_results: 'a T list -> 'a Exn.result list
   val join: 'a T -> 'a
-  val release_results: 'a Exn.result list -> 'a list
   val focus: task list -> unit
   val interrupt_task: string -> unit
   val cancel: 'a T -> unit
@@ -236,7 +235,7 @@
     val result = ref (NONE: 'a Exn.result option);
     val run = Multithreading.with_attributes (Thread.getAttributes ())
       (fn _ => fn ok =>
-        let val res = if ok then Exn.capture e () else Exn.Exn Interrupt
+        let val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt
         in result := SOME res; is_some (Exn.get_result res) end);
 
     val task = SYNCHRONIZED "future" (fn () =>
@@ -288,18 +287,6 @@
 fun join x = Exn.release (singleton join_results x);
 
 
-(* release results *)
-
-fun proper_exn (Exn.Result _) = NONE
-  | proper_exn (Exn.Exn Interrupt) = NONE
-  | proper_exn (Exn.Exn exn) = SOME exn;
-
-fun release_results results =
-  (case get_first proper_exn results of
-    SOME exn => raise exn
-  | NONE => List.map Exn.release results);
-
-
 (* misc operations *)
 
 (*focus: collection of high-priority task*)