src/HOL/Tools/Sledgehammer/sledgehammer.ML

              Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
                  (Pretty.str message)]))
       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);
        (false, state))
   end

             fold (fn prover => fn (true, state) => (true, state)
                                 | (false, _) => run_prover prover)
                  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
 
 val setup =