1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu May 22 03:29:35 2014 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu May 22 03:29:35 2014 +0200
     1.3 @@ -269,24 +269,19 @@
     1.4  
     1.5  \prew
     1.6  \slshape
     1.7 -Sledgehammer: ``\textit{e\/}'' on goal \\
     1.8 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
     1.9 +Sledgehammer: ``\textit{e\/}'' \\
    1.10  Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
    1.11  %
    1.12 -Sledgehammer: ``\textit{z3\/}'' on goal \\
    1.13 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.14 +Sledgehammer: ``\textit{z3\/}'' \\
    1.15  Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
    1.16  %
    1.17 -Sledgehammer: ``\textit{vampire\/}'' on goal \\
    1.18 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.19 +Sledgehammer: ``\textit{vampire\/}'' \\
    1.20  Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
    1.21  %
    1.22 -Sledgehammer: ``\textit{spass\/}'' on goal \\
    1.23 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.24 +Sledgehammer: ``\textit{spass\/}'' \\
    1.25  Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
    1.26  %
    1.27 -Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
    1.28 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.29 +Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\
    1.30  Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
    1.31  \postw
    1.32  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 03:29:35 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 03:29:35 2014 +0200
     2.3 @@ -54,15 +54,9 @@
     2.4         ordered_outcome_codes
     2.5    |> the_default unknownN
     2.6  
     2.7 -fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
     2.8 +fun prover_description verbose name num_facts =
     2.9    (quote name,
    2.10 -   (if verbose then
    2.11 -      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    2.12 -    else
    2.13 -      "") ^
    2.14 -   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
    2.15 -   (if blocking then "."
    2.16 -    else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    2.17 +   if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
    2.18  
    2.19  fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
    2.20      output_result minimize_command only learn
    2.21 @@ -77,8 +71,6 @@
    2.22      val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
    2.23      val num_facts = length facts |> not only ? Integer.min max_facts
    2.24  
    2.25 -    fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
    2.26 -
    2.27      val problem =
    2.28        {comment = comment, state = state, goal = goal, subgoal = subgoal,
    2.29         subgoal_count = subgoal_count,
    2.30 @@ -195,7 +187,8 @@
    2.31              |> List.app Output.urgent_message
    2.32        in (outcome_code, state) end
    2.33      else
    2.34 -      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
    2.35 +      (Async_Manager.thread SledgehammerN birth_time death_time
    2.36 +         (prover_description verbose name num_facts)
    2.37           ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
    2.38         (unknownN, state))
    2.39    end