src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

       smt2_filter_loop name params state goal subgoal factss
     val used_named_facts = map snd fact_ids
     val used_facts = map fst used_named_facts
     val outcome = Option.map failure_of_smt2_failure outcome
 
-    val (preferred_methss, message, message_tail) =
+    val (preferred_methss, message) =
       (case outcome of
         NONE =>
         let
           val preferred_methss =
             (SMT2_Method, bunches_of_proof_methods (smt_proofs <> SOME false) false liftingN)

 
                val one_line_params =
                  (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
-               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
-             end,
-           if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
+               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
+                 one_line_params
+             end)
         end
-      | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure, ""))
+      | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
   in
     {outcome = outcome, used_facts = used_facts, used_from = used_from,
-     preferred_methss = preferred_methss, run_time = run_time, message = message,
-     message_tail = message_tail}
+     preferred_methss = preferred_methss, run_time = run_time, message = message}
   end
 
 end;