tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;

--- a/src/Pure/Concurrent/future.ML	Wed Feb 09 08:42:23 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Feb 09 15:48:43 2011 +0100
@@ -182,8 +182,8 @@
           if ok then
             Exn.capture (fn () =>
               Multithreading.with_attributes Multithreading.private_interrupts
-                (fn _ =>
-                  Position.setmp_thread_data pos e () before Multithreading.interrupted ())) ()
+                (fn _ => Position.setmp_thread_data pos e ()) before
+              Multithreading.interrupted ()) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;