# HG changeset patch
# User wenzelm
# Date 1459955825 -7200
# Node ID 7485507620b677315da860b7a83acf61854b2aad
# Parent  7a11ea5c96266232f52453d541f03c72b8f471fd
unused;

diff -r 7a11ea5c9626 -r 7485507620b6 src/Pure/Concurrent/multithreading.ML
--- 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);