--- a/src/Pure/Concurrent/multithreading.ML Wed Apr 06 17:16:30 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Wed Apr 06 17:17:05 2016 +0200
@@ -12,7 +12,6 @@
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 interruptible: ('a -> 'b) -> 'a -> 'b
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
val max_threads_value: unit -> int
val max_threads_update: int -> unit
@@ -70,8 +69,6 @@
val _ = Thread.setAttributes orig_atts;
in Exn.release result end;
-fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
-
fun uninterruptible f x =
with_attributes no_interrupts (fn atts =>
f (fn g => fn y => with_attributes atts (fn _ => g y)) x);