tuned signature;

--- 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] =
   {

--- a/src/Pure/Concurrent/standard_thread.scala	Tue Nov 03 17:41:13 2015 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala	Tue Nov 03 17:53:09 2015 +0100
@@ -9,13 +9,14 @@
 
 
 import java.lang.Thread
-import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
-  TimeUnit, LinkedBlockingQueue}
+import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue}
+
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutor}
 
 
 object Standard_Thread
 {
-  /* plain thread */
+  /* fork */
 
   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
   {
@@ -28,7 +29,7 @@
   }
 
 
-  /* thread pool */
+  /* pool */
 
   lazy val pool: ThreadPoolExecutor =
     {
@@ -37,8 +38,8 @@
       new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
     }
 
-  def submit_task[A](body: => A): JFuture[A] =
-    pool.submit(new Callable[A] { def call = body })
+  lazy val execution_context: ExecutionContextExecutor =
+    ExecutionContext.fromExecutorService(pool)
 
 
   /* delayed events */