src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Mon Feb 07 23:57:03 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Tue Feb 08 14:09:24 2011 +0100
@@ -21,6 +21,7 @@
   val public_interrupts: Thread.threadAttribute list
   val private_interrupts: Thread.threadAttribute list
   val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+  val interrupted: unit -> unit  (*exception Interrupt*)
   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
@@ -50,6 +51,8 @@
 val private_interrupts = [];
 fun sync_interrupts _ = [];
 
+fun interrupted () = ();
+
 fun with_attributes _ e = e [];
 
 fun sync_wait _ _ _ _ = Exn.Result true;