diff -r 264c7488d532 -r 91c3aedbfc5e src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala Tue Nov 03 17:41:13 2015 +0100 +++ b/src/Pure/Concurrent/future.scala Tue Nov 03 17:53:09 2015 +0100 @@ -8,6 +8,9 @@ package isabelle +import java.util.concurrent.Callable + + /* futures and promises */ object Future @@ -85,7 +88,7 @@ status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result)) } } - private val task = Standard_Thread.submit_task { try_run() } + private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body }) def join_result: Exn.Result[A] = {