eliminated needlessly complex message tail

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -157,13 +157,13 @@
           print_used_facts used_facts used_from
         | _ => ())
       |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
-      |> (fn {outcome, used_facts, used_from, preferred_methss, message, message_tail, ...} =>
+      |> (fn {outcome, used_facts, used_from, preferred_methss, message, ...} =>
         (if outcome = SOME ATP_Proof.TimedOut then timeoutN
          else if is_some outcome then noneN
          else someN,
          fn () => message (play_one_line_proof mode preplay_timeout
            (filter_used_facts false used_facts used_from) state subgoal
-           preferred_methss) ^ message_tail))
+           preferred_methss)))
 
     fun go () =
       let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -58,8 +58,7 @@
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      run_time : Time.time,
-     message : proof_method * play_outcome -> string,
-     message_tail : string}
+     message : proof_method * play_outcome -> string}
 
   type prover = params -> prover_problem -> prover_result
 
@@ -150,8 +149,7 @@
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    run_time : Time.time,
-   message : proof_method * play_outcome -> string,
-   message_tail : string}
+   message : proof_method * play_outcome -> string}
 
 type prover = params -> prover_problem -> prover_result
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -127,8 +127,7 @@
    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
@@ -354,7 +353,7 @@
       else
         ""
 
-    val (used_facts, preferred_methss, message, message_tail) =
+    val (used_facts, preferred_methss, message) =
       (case outcome of
         NONE =>
         let
@@ -390,20 +389,19 @@
                   (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;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -22,12 +22,8 @@
   val binary_min_facts : int Config.T
   val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
     Proof.state -> thm -> ((string * stature) * thm list) list ->
-    ((string * stature) * thm list) list option
-     * (((proof_method * play_outcome) -> string) * string)
+    ((string * stature) * thm list) list option * ((proof_method * play_outcome) -> string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
-
-  val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
-    Proof.state -> unit
 end;
 
 structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE =
@@ -209,8 +205,7 @@
          val min =
            if length facts >= Config.get ctxt binary_min_facts then binary_minimize
            else linear_minimize
-         val (min_facts, {message, message_tail, ...}) =
-           min test (new_timeout timeout run_time) result facts
+         val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result facts
        in
          print silent (fn () => cat_lines
              ["Minimized to " ^ n_facts (map fst min_facts)] ^
@@ -218,38 +213,37 @@
                  0 => ""
                | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
          (if learn then do_learn (maps snd min_facts) else ());
-         (SOME min_facts, (message, message_tail))
+         (SOME min_facts, message)
        end
      | {outcome = SOME TimedOut, ...} =>
-       (NONE, (fn _ =>
+       (NONE, fn _ =>
           "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
-          \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
-     | {message, ...} => (NONE, (prefix "Prover error: " o message, ""))))
-    handle ERROR msg => (NONE, (fn _ => "Error: " ^ msg, ""))
+          \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").")
+     | {message, ...} => (NONE, (prefix "Prover error: " o message))))
+    handle ERROR msg => (NONE, fn _ => "Error: " ^ msg)
   end
 
 fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
     ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
-    (result as {outcome, used_facts, used_from, preferred_methss, run_time, message, message_tail}
+    (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
      : prover_result) =
   if is_some outcome orelse null used_facts then
     result
   else
     let
-      val (used_facts, (message, _)) =
+      val (used_facts, message) =
         if minimize then
           minimize_facts do_learn name params
             (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
             goal (filter_used_facts true used_facts (map (apsnd single) used_from))
           |>> Option.map (map fst)
         else
-          (SOME used_facts, (message, ""))
+          (SOME used_facts, message)
     in
       (case used_facts of
         SOME used_facts =>
         {outcome = NONE, 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}
       | NONE => result)
     end
 
@@ -257,25 +251,4 @@
   get_prover ctxt mode name params problem
   |> maybe_minimize mode do_learn name params problem
 
-fun run_minimize (params as {provers, ...}) do_learn i refs state =
-  let
-    val ctxt = Proof.context_of state
-    val {goal, facts = chained_ths, ...} = Proof.goal state
-    val reserved = reserved_isar_keyword_table ()
-    val css = clasimpset_rule_table_of ctxt
-    val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css)
-  in
-    (case subgoal_count state of
-      0 => Output.urgent_message "No subgoal!"
-    | n =>
-      (case provers of
-        [] => error "No prover is set."
-      | prover :: _ =>
-        (kill_provers ();
-         minimize_facts do_learn prover params false i n state goal facts
-         |> (fn (_, (message, message_tail)) =>
-           Output.urgent_message (message (Metis_Method (NONE, NONE),
-             Play_Timed_Out Time.zeroTime) ^ message_tail)))))
-  end
-
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -192,7 +192,7 @@
     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
@@ -212,15 +212,14 @@
                  (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;