# HG changeset patch
# User blanchet
# Date 1400722175 -7200
# Node ID 46000c075d07961a878b63dfe8046d487334e04e
# Parent  ea5912e3b00819294d40f47ee9941d2597b61fa9
shorten Sledgehammer output, as suggested by Andrei Popescu

diff -r ea5912e3b008 -r 46000c075d07 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu May 22 03:29:35 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu May 22 03:29:35 2014 +0200
@@ -269,24 +269,19 @@
 
 \prew
 \slshape
-Sledgehammer: ``\textit{e\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{e\/}'' \\
 Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{z3\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{z3\/}'' \\
 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{vampire\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{vampire\/}'' \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{spass\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{spass\/}'' \\
 Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
 \postw
 
diff -r ea5912e3b008 -r 46000c075d07 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 03:29:35 2014 +0200
@@ -54,15 +54,9 @@
        ordered_outcome_codes
   |> the_default unknownN
 
-fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
+fun prover_description verbose name num_facts =
   (quote name,
-   (if verbose then
-      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
-    else
-      "") ^
-   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
-   (if blocking then "."
-    else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
+   if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
 
 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
     output_result minimize_command only learn
@@ -77,8 +71,6 @@
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length facts |> not only ? Integer.min max_facts
 
-    fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
-
     val problem =
       {comment = comment, state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count,
@@ -195,7 +187,8 @@
             |> List.app Output.urgent_message
       in (outcome_code, state) end
     else
-      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
+      (Async_Manager.thread SledgehammerN birth_time death_time
+         (prover_description verbose name num_facts)
          ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
        (unknownN, state))
   end