diff -r 591fefcf184e -r cb6421b6a18f src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Fri Mar 20 20:05:51 2009 +0100 +++ b/src/Pure/Concurrent/future.ML Fri Mar 20 20:20:09 2009 +0100 @@ -236,7 +236,7 @@ fun future_job group (e: unit -> 'a) = let val result = ref (NONE: 'a Exn.result option); - val job = Multithreading.with_attributes (Thread.getAttributes ()) + val job = Multithreading.with_attributes Multithreading.restricted_interrupts (fn _ => fn ok => let val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;