# HG changeset patch
# User wenzelm
# Date 1223578390 -7200
# Node ID 637f2808ab647bc6015402e9d0cceba465d33196
# Parent  86b39d27b199c0fdd0a651072b3c39a163d67c06
SimpleThread.interrupt;

diff -r 86b39d27b199 -r 637f2808ab64 src/HOL/Tools/atp_manager.ML
--- 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 =
diff -r 86b39d27b199 -r 637f2808ab64 src/Pure/Concurrent/schedule.ML
--- 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 ())));