src/Pure/Concurrent/thread_data_virtual.ML
changeset 78716 97dfba4405e3
parent 74561 8e6c973003c8
child 78720 909dc00766a0
--- a/src/Pure/Concurrent/thread_data_virtual.ML	Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/thread_data_virtual.ML	Tue Sep 26 12:46:31 2023 +0200
@@ -30,11 +30,11 @@
     | SOME x => Inttab.update (i, Universal.tagInject tag x));
 
 fun setmp v data f x =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn run => fn () =>
     let
       val orig_data = get v;
       val _ = put v data;
-      val result = Exn.capture (restore_attributes f) x;
+      val result = Exn.capture (run f) x;
       val _ = put v orig_data;
     in Exn.release result end) ();