# HG changeset patch
# User wenzelm
# Date 1481711183 -3600
# Node ID fc66a76d6b9501c840731433fb99a7ce164243af
# Parent  20e361014f55c4dc0aa4155e168a9eba4b8e8875
tuned;

diff -r 20e361014f55 -r fc66a76d6b95 src/Pure/Concurrent/thread_attributes.ML
--- a/src/Pure/Concurrent/thread_attributes.ML	Wed Dec 14 10:40:25 2016 +0100
+++ b/src/Pure/Concurrent/thread_attributes.ML	Wed Dec 14 11:26:23 2016 +0100
@@ -88,14 +88,20 @@
     val w'' = Word.andb (w, Word.notb interrupt_state);
   in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;
 
-end;
-
 fun with_attributes new_atts e =
   let
-    val orig_atts = safe_interrupts (get_attributes ());
-    val result = Exn.capture (fn () => (set_attributes (safe_interrupts new_atts); e orig_atts)) ();
-    val _ = set_attributes orig_atts;
-  in Exn.release result end;
+    val atts1 = safe_interrupts (get_attributes ());
+    val atts2 = safe_interrupts new_atts;
+  in
+    if atts1 = atts2 then e atts1
+    else
+      let
+        val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
+        val _ = set_attributes atts1;
+      in Exn.release result end
+  end;
+
+end;
 
 fun uninterruptible f x =
   with_attributes no_interrupts (fn atts =>