src/Pure/Concurrent/simple_thread.ML
changeset 33220 11a1af478dac
parent 32298 400cc493d466
child 33602 d25e6bd6ca95
     1.1 --- a/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 10:54:25 2009 +0100
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 11:25:56 2009 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  struct
     1.5  
     1.6  fun fork interrupts body =
     1.7 -  Thread.fork (fn () => exception_trace (fn () => body ()),
     1.8 +  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     1.9      if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
    1.10  
    1.11  fun interrupt thread = Thread.interrupt thread handle Thread _ => ();