src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32107 47d0da617fcc
parent 31897 15d55d07de8b
child 32184 cfa0ef0c0c5f
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 21 20:37:32 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 21 23:42:29 2009 +0200
     1.3 @@ -92,10 +92,12 @@
     1.4      val _ = Thread.setAttributes orig_atts;
     1.5    in Exn.release result end;
     1.6  
     1.7 -fun interruptible f = with_attributes regular_interrupts (fn _ => f);
     1.8 +fun interruptible f =
     1.9 +  with_attributes regular_interrupts (fn _ => fn x => f x);
    1.10  
    1.11  fun uninterruptible f =
    1.12 -  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
    1.13 +  with_attributes no_interrupts (fn atts => fn x =>
    1.14 +    f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
    1.15  
    1.16  
    1.17  (* execution with time limit *)