src/Pure/ML-Systems/multithreading.ML

   val enabled: unit -> bool
   val no_interrupts: Thread.threadAttribute list
   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
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit

 
 val no_interrupts = [];
 val public_interrupts = [];
 val private_interrupts = [];
 fun sync_interrupts _ = [];
+
+fun interrupted () = ();
 
 fun with_attributes _ e = e [];
 
 fun sync_wait _ _ _ _ = Exn.Result true;