src/Pure/System/invoke_scala.scala

--- a/src/Pure/System/invoke_scala.scala	Fri Apr 25 20:21:27 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala	Fri Apr 25 21:31:39 2014 +0200
@@ -8,6 +8,8 @@
 
 
 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+import java.util.concurrent.{Future => JFuture}
+
 import scala.util.matching.Regex
 
 
@@ -70,7 +72,7 @@
 
 class Invoke_Scala extends Session.Protocol_Handler
 {
-  private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
+  private var futures = Map.empty[String, JFuture[Unit]]
 
   private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
     synchronized
@@ -81,7 +83,7 @@
       }
     }
 
-  private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
+  private def cancel(prover: Prover, id: String, future: JFuture[Unit])
   {
     future.cancel(true)
     fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
@@ -92,11 +94,10 @@
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
-          default_thread_pool.submit(() =>
-            {
-              val (tag, result) = Invoke_Scala.method(name, msg.text)
-              fulfill(prover, id, tag, result)
-            }))
+          Simple_Thread.submit_task {
+            val (tag, result) = Invoke_Scala.method(name, msg.text)
+            fulfill(prover, id, tag, result)
+          })
         true
       case _ => false
     }