src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be
    the only ATP that does not honor its time limit. *)
 val atp_timeout_slack = seconds 1.0
 
-(* Important messages are important but not so important that users want to see
-   them each time. *)
+(* Important messages are important but not so important that users want to see them each time. *)
 val atp_important_message_keep_quotient = 25
 
 fun run_atp mode name
     ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,

       if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
         extract_important_message output
       else
         ""
 
-    val (used_facts, preferred_methss, message, message_tail) =
+    val (used_facts, preferred_methss, message) =
       (case outcome of
         NONE =>
         let
           val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof

 
                 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 "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
-           (if important_message <> "" then
-              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
-            else
-              ""))
+                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
+                  one_line_params ^
+                (if important_message <> "" then
+                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
+                 else
+                   "")
+              end)
         end
       | SOME failure =>
-        ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure 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;