# HG changeset patch
# User blanchet
# Date 1283784629 -7200
# Node ID 8420a873f534b6a7bc442315c4c197de7f7293e9
# Parent  2aca183ef915d1f1ba68b87f24392facdc7f6e92
use Future.fork rather than Thread.fork, so that the thread is part of the global thread management

diff -r 2aca183ef915 -r 8420a873f534 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Sep 06 13:48:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Sep 06 16:50:29 2010 +0200
@@ -452,7 +452,7 @@
             else
               ()
           end
-      in if blocking then run () else Toplevel.thread true (tap run) |> K () end
+      in if blocking then run () else Future.fork run |> K () end
 
 val setup =
   dest_dir_setup