src/HOL/Tools/Sledgehammer/sledgehammer.ML

         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
             (full_types, minimize_command, proof, axiom_names, goal, subgoal)
         |>> (fn message =>
                 message ^ (if verbose then
-                             "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
+                             "\nCPU time: " ^ string_of_int msecs ^ " ms."
                            else
                              ""))
       | SOME failure => (string_for_failure failure, [])
   in
     {outcome = outcome, message = message, pool = pool,

      conjecture_shape = conjecture_shape}
   end
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
-fun start_prover_thread (params as {blocking, timeout, expect, ...})
-                        i n relevance_override minimize_command axioms state
-                        (prover, atp_name) =
+fun run_prover ctxt (params as {blocking, timeout, expect, ...}) i n
+               relevance_override minimize_command
+               (problem as {goal, ...}) (prover, atp_name) =
   let
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
-    val {context = ctxt, facts, goal} = Proof.goal state
     val desc =
       "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":" ^
       (if blocking then
          ""
        else
          "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
     fun run () =
       let
-        val problem =
-          {ctxt = ctxt, goal = goal, subgoal = i,
-           axioms = map (prepare_axiom ctxt) axioms}
         val (outcome_code, message) =
           prover_fun atp_name prover params (minimize_command atp_name) problem
           |> (fn {outcome, message, ...} =>
                  (if is_some outcome then "none" else "some", message))
           handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")

                              provers 0
             val axioms =
               relevant_facts ctxt full_types relevance_thresholds
                              max_max_relevant relevance_override chained_ths
                              hyp_ts concl_t
+            val problem =
+              {ctxt = ctxt, goal = goal, subgoal = i,
+               axioms = map (prepare_axiom ctxt) axioms}
             val num_axioms = length axioms
             val _ = if verbose then
                       priority ("Selected " ^ string_of_int num_axioms ^
                                 " fact" ^ plural_s num_axioms ^ ".")
                     else
                       ()
             val _ =
               (if blocking then Par_List.map else map)
-                  (start_prover_thread params i n relevance_override
-                                       minimize_command axioms state) provers
+                  (run_prover ctxt params i n relevance_override
+                              minimize_command problem) provers
           in
             if verbose andalso blocking then
               priority ("Total time: " ^
                         signed_string_of_int (Time.toMilliseconds
                             (Timer.checkRealTimer timer)) ^ " ms.")