diff -r ee564db2649b -r 97964515a676 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Thu Sep 20 19:23:05 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Thu Sep 20 20:13:42 2012 +0200
@@ -15,6 +15,12 @@
 
 object Simple_Thread
 {
+  /* prending interrupts */
+
+  def interrupted_exception(): Unit =
+    if (Thread.interrupted()) throw new InterruptedException
+
+
   /* plain thread */
 
   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =