src/Pure/Concurrent/synchronized.ML
changeset 78720 909dc00766a0
parent 78650 47d0c333d155
child 80073 40f5ddeda2b4
--- a/src/Pure/Concurrent/synchronized.ML	Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue Sep 26 14:42:33 2023 +0200
@@ -57,9 +57,9 @@
         (case ! state of
           Immutable _ => immutable_fail name
         | Mutable _ =>
-            Thread_Attributes.uninterruptible (fn _ => fn () =>
+            Thread_Attributes.uninterruptible_body (fn _ =>
              (state := Immutable x; RunCall.clearMutableBit state;
-               Thread.ConditionVar.broadcast cond)) ())));
+               Thread.ConditionVar.broadcast cond)))));
 
 
 (* synchronized access *)
@@ -81,9 +81,9 @@
                     | Exn.Res false => NONE
                     | Exn.Exn exn => Exn.reraise exn)
                 | SOME (y, x') =>
-                    Thread_Attributes.uninterruptible (fn _ => fn () =>
+                    Thread_Attributes.uninterruptible_body (fn _ =>
                       (state := Mutable {lock = lock, cond = cond, content = x'};
-                        Thread.ConditionVar.broadcast cond; SOME y)) ()));
+                        Thread.ConditionVar.broadcast cond; SOME y))));
         in try_change () end));
 
 fun guarded_access var f = the (timed_access var (fn _ => NONE) f);