--- 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 =