src/Pure/Concurrent/multithreading.ML
changeset 78715 9506b852ebdf
parent 78650 47d0c333d155
child 78716 97dfba4405e3
--- a/src/Pure/Concurrent/multithreading.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -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.capture (restore_attributes e) ();
+        val result = Exn.capture0 (restore_attributes 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.capture (restore_attributes e) ();
+        val result = Exn.capture0 (restore_attributes e) ();
         val _ = Thread.Mutex.unlock lock;
       in result end) ());