SimpleThread.interrupt;

--- a/src/HOL/Tools/atp_manager.ML	Thu Oct 09 20:03:22 2008 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Thu Oct 09 20:53:10 2008 +0200
@@ -84,10 +84,8 @@
             cancelolder (ThreadHeap.delete_min heap))
           end
         val _ = change timeout_heap cancelolder
-        (* try to interrupt threads that are to cancel*)
-        fun interrupt t = Thread.interrupt t handle Thread _ => ()
         val _ = change cancelling (filter (fn (t,_,_,_) => Thread.isActive t))
-        val _ = map (fn (t, _, _, _) => interrupt t) (! cancelling)
+        val _ = map (fn (t, _, _, _) => SimpleThread.interrupt t) (! cancelling)
         (* if there are threads to cancel, send periodic interrupts *)
         (* TODO: find out what realtime-values are appropriate *)
         val next_time =

--- a/src/Pure/Concurrent/schedule.ML	Thu Oct 09 20:03:22 2008 +0200
+++ b/src/Pure/Concurrent/schedule.ML	Thu Oct 09 20:53:10 2008 +0200
@@ -76,7 +76,7 @@
       while not (null (! running)) do
       (trace_active ();
        if not (null (! status))
-       then (List.app (fn t => Thread.interrupt t handle Thread _ => ()) (! running))
+       then (List.app SimpleThread.interrupt (! running))
        else ();
        wait_timeout ())));