1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 17:46:40 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 17:46:41 2008 +0200
     1.3 @@ -82,10 +82,11 @@
     1.4      [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]
     1.5      (fn _ => f);
     1.6  
     1.7 +val no_interrupts =
     1.8 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
     1.9 +
    1.10  fun uninterruptible f =
    1.11 -  with_attributes
    1.12 -    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]
    1.13 -    (fn atts => f (fn g => with_attributes atts (fn _ => g)));
    1.14 +  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
    1.15  
    1.16  
    1.17  (* execution with time limit *)
    1.18 @@ -193,7 +194,7 @@
    1.19  fun self_critical () =
    1.20    (case ! critical_thread of
    1.21      NONE => false
    1.22 -  | SOME id => Thread.equal (id, Thread.self ()));
    1.23 +  | SOME t => Thread.equal (t, Thread.self ()));
    1.24  
    1.25  fun NAMED_CRITICAL name e =
    1.26    if self_critical () then e ()