src/Pure/Concurrent/multithreading.ML
changeset 78716 97dfba4405e3
parent 78715 9506b852ebdf
child 78720 909dc00766a0
--- a/src/Pure/Concurrent/multithreading.ML	Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Tue Sep 26 12:46:31 2023 +0200
@@ -83,7 +83,7 @@
 (* synchronized evaluation *)
 
 fun synchronized name lock e =
-  Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Exn.release (Thread_Attributes.uninterruptible (fn run => fn () =>
     if ! trace > 0 then
       let
         val immediate =
@@ -96,14 +96,14 @@
               val time = Timer.checkRealTimer timer;
               val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
             in false end;
-        val result = Exn.capture0 (restore_attributes e) ();
+        val result = Exn.capture0 (run e) ();
         val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
         val _ = Thread.Mutex.unlock lock;
       in result end
     else
       let
         val _ = Thread.Mutex.lock lock;
-        val result = Exn.capture0 (restore_attributes e) ();
+        val result = Exn.capture0 (run e) ();
         val _ = Thread.Mutex.unlock lock;
       in result end) ());