src/Pure/Concurrent/thread_attributes.ML

--- a/src/Pure/Concurrent/thread_attributes.ML	Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/thread_attributes.ML	Tue Sep 26 14:42:33 2023 +0200
@@ -18,6 +18,7 @@
   val safe_interrupts: attributes -> attributes
   val with_attributes: attributes -> (attributes -> 'a) -> 'a
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+  val uninterruptible_body: ((('b -> 'c) -> 'b -> 'c) -> 'a) -> 'a
 end;
 
 structure Thread_Attributes: THREAD_ATTRIBUTES =
@@ -106,4 +107,7 @@
   with_attributes no_interrupts (fn atts =>
     f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
 
+fun uninterruptible_body body =
+  uninterruptible (fn run => fn () => body run) ();
+
 end;