--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Sep 14 19:38:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Sep 14 19:38:44 2010 +0200
@@ -422,7 +422,9 @@
end
else if blocking then
let val (success, message) = TimeLimit.timeLimit timeout go () in
- priority (desc ^ "\n" ^ message); (success, state)
+ List.app priority
+ (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
+ (success, state)
end
else
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
@@ -472,13 +474,6 @@
provers (false, state)
else
(if blocking then Par_List.map else map) run_prover provers
- |> tap (fn _ =>
- if verbose then
- priority ("Total time: " ^
- signed_string_of_int (Time.toMilliseconds
- (Timer.checkRealTimer timer)) ^ " ms.")
- else
- ())
|> exists fst |> rpair state
end
in if blocking then go () else Future.fork (tap go) |> K (false, state) end