diff -r 82339c3fd74a -r a21084741b37 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Feb 07 23:57:03 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 08 14:09:24 2011 +0100
@@ -45,6 +45,9 @@
 val no_interrupts =
   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
 
+val test_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
 val public_interrupts =
   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
 
@@ -61,6 +64,14 @@
       Thread.InterruptState Thread.InterruptAsynchOnce
     | x => x);
 
+fun interrupted () =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val _ = Thread.setAttributes test_interrupts;
+    val test = Exn.capture Thread.testInterrupt ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release test end;
+
 fun with_attributes new_atts e =
   let
     val orig_atts = safe_interrupts (Thread.getAttributes ());