# HG changeset patch
# User wenzelm
# Date 1223046461 -7200
# Node ID 8b6af52424f6637ca0a5ef61cce72b69366b6f3b
# Parent  855ca2dcc03da1884a5a9d90fe5c9e7c1fa664be
simplified thread creation via SimpleThread;

diff -r 855ca2dcc03d -r 8b6af52424f6 src/HOL/Tools/atp_thread.ML
--- a/src/HOL/Tools/atp_thread.ML	Fri Oct 03 17:07:39 2008 +0200
+++ b/src/HOL/Tools/atp_thread.ML	Fri Oct 03 17:07:41 2008 +0200
@@ -51,16 +51,14 @@
     unregistering is done by thread.
   *)
   fun atp_thread call_prover action_success description =
-    let val thread = Thread.fork(fn () =>
+    let val thread = SimpleThread.fork true (fn () =>
       let
       val answer = call_prover ()
       val _ = if isSome answer then action_success (valOf answer)
         else delayed_priority ("Sledgehammer: " ^ description ^ "\n  failed.")
       in AtpManager.unregister (isSome answer)
       end
-      handle Interrupt => delayed_priority ("Sledgehammer: " ^ description ^ "\n  interrupted.")
-    ,[Thread.EnableBroadcastInterrupt true,
-     Thread.InterruptState Thread.InterruptAsynch])
+      handle Interrupt => delayed_priority ("Sledgehammer: " ^ description ^ "\n  interrupted."))
     in (thread, description) end
 
   (* Settings for path and filename to problemfiles *)