src/Pure/Concurrent/thread_attributes.ML
changeset 78713 a44ac17ae227
parent 64564 fc66a76d6b95
child 78715 9506b852ebdf
--- a/src/Pure/Concurrent/thread_attributes.ML	Mon Sep 25 21:36:46 2023 +0200
+++ b/src/Pure/Concurrent/thread_attributes.ML	Mon Sep 25 21:46:38 2023 +0200
@@ -18,7 +18,6 @@
   val safe_interrupts: attributes -> attributes
   val with_attributes: attributes -> (attributes -> 'a) -> 'a
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val expose_interrupt: unit -> unit  (*exception Interrupt*)
 end;
 
 structure Thread_Attributes: THREAD_ATTRIBUTES =
@@ -107,12 +106,4 @@
   with_attributes no_interrupts (fn atts =>
     f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
 
-fun expose_interrupt () =
-  let
-    val orig_atts = safe_interrupts (get_attributes ());
-    val _ = set_attributes test_interrupts;
-    val test = Exn.capture Thread.Thread.testInterrupt ();
-    val _ = set_attributes orig_atts;
-  in Exn.release test end;
-
 end;