# HG changeset patch
# User wenzelm
# Date 1368783352 -7200
# Node ID 9003b293e775592d6dc2f9003d8eed184f1eefb2
# Parent  0476162187c484920f4dc2adca01efc12016689e
tuned signature -- emphasize thread creation here;

diff -r 0476162187c4 -r 9003b293e775 src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 17 11:05:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 17 11:35:52 2013 +0200
@@ -9,7 +9,7 @@
 signature ASYNC_MANAGER =
 sig
   val break_into_chunks : string -> string list
-  val launch :
+  val thread :
     string -> Time.time -> Time.time -> string * string
     -> (unit -> bool * string) -> unit
   val kill_threads : string -> string -> unit
@@ -180,7 +180,7 @@
   check_thread_manager ())
 
 
-fun launch tool birth_time death_time desc f =
+fun thread tool birth_time death_time desc f =
   (Toplevel.thread true
        (fn () =>
            let
diff -r 0476162187c4 -r 9003b293e775 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 17 11:05:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 17 11:35:52 2013 +0200
@@ -883,7 +883,7 @@
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
     val desc = ("Machine learner for Sledgehammer", "")
-  in Async_Manager.launch MaShN birth_time death_time desc task end
+  in Async_Manager.thread MaShN birth_time death_time desc task end
 
 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
                      used_ths =
diff -r 0476162187c4 -r 9003b293e775 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 17 11:05:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 17 11:35:52 2013 +0200
@@ -157,7 +157,7 @@
         (outcome_code, state)
       end
     else
-      (Async_Manager.launch SledgehammerN birth_time death_time (desc ())
+      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
                             ((fn (outcome_code, message) =>
                                  (verbose orelse outcome_code = someN,
                                   message ())) o go);