diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/thread_data_virtual.ML --- 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) ();