src/HOL/Tools/Sledgehammer/sledgehammer.ML

      overlord: bool,
      atps: string list,
      full_types: bool,
      explicit_apply: bool,
      relevance_threshold: real,
-     relevance_decay: real,
-     max_relevant_per_iter: int option,
+     relevance_decay: real option,
+     max_relevant: int option,
      theory_relevant: bool option,
      isar_proof: bool,
      isar_shrink_factor: int,
      timeout: Time.time}
   type problem =

    overlord: bool,
    atps: string list,
    full_types: bool,
    explicit_apply: bool,
    relevance_threshold: real,
-   relevance_decay: real,
-   max_relevant_per_iter: int option,
+   relevance_decay: real option,
+   max_relevant: int option,
    theory_relevant: bool option,
    isar_proof: bool,
    isar_shrink_factor: int,
    timeout: Time.time}
 

     let
       val j0 = hd (hd conjecture_shape)
       val seq = extract_clause_sequence output
       val name_map = extract_clause_formula_relation output
       fun renumber_conjecture j =
-        conjecture_prefix ^ Int.toString (j - j0)
+        conjecture_prefix ^ string_of_int (j - j0)
         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
         |> map (fn s => find_index (curry (op =) s) seq + 1)
       fun name_for_number j =
         let
           val axioms =

 
 (* generic TPTP-based provers *)
 
 fun prover_fun atp_name
         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
-         known_failures, default_max_relevant_per_iter, default_theory_relevant,
+         known_failures, default_max_relevant, default_theory_relevant,
          explicit_forall, use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
-          relevance_threshold, relevance_decay,
-          max_relevant_per_iter, theory_relevant, isar_proof,
-          isar_shrink_factor, timeout, ...} : params)
+          relevance_threshold, relevance_decay, max_relevant, theory_relevant,
+          isar_proof, isar_shrink_factor, timeout, ...} : params)
         minimize_command
         ({subgoal, goal, relevance_override, axioms} : problem) =
   let
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt
     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
 
-    fun print s = (priority s; if debug then tracing s else ())
+    val print = priority
     fun print_v f = () |> verbose ? print o f
     fun print_d f = () |> debug ? print o f
 
     val the_axioms =
       case axioms of
         SOME axioms => axioms
       | NONE =>
         (relevant_facts full_types relevance_threshold relevance_decay
-                        (the_default default_max_relevant_per_iter
-                                     max_relevant_per_iter)
+                        (the_default default_max_relevant max_relevant)
                         (the_default default_theory_relevant theory_relevant)
                         relevance_override goal hyp_ts concl_t
          |> tap ((fn n => print_v (fn () =>
                       "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
                       " for " ^ quote atp_name ^ ".")) o length))

         else if File.exists (Path.explode the_dest_dir)
         then Path.append (Path.explode the_dest_dir) probfile
         else error ("No such directory: " ^ the_dest_dir ^ ".")
       end;
 
+    val measure_run_time = verbose orelse Config.get ctxt measure_runtime
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     (* write out problem file and call prover *)
     fun command_line complete timeout probfile =
       let
         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
                    " " ^ File.shell_path probfile
       in
-        (if Config.get ctxt measure_runtime then
-           "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
-         else
-           "exec " ^ core) ^ " 2>&1"
+        (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
+         else "exec " ^ core) ^ " 2>&1"
       end
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");
         val (output, t) = s |> split |> split_last |> apfst cat_lines;

                   bash_output command
                   |>> (if overlord then
                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
                        else
                          I)
-                  |>> (if Config.get ctxt measure_runtime then split_time
-                       else rpair 0)
+                  |>> (if measure_run_time then split_time else rpair 0)
                 val (proof, outcome) =
                   extract_proof_and_outcome complete res_code proof_delims
                                             known_failures output
               in (output, msecs, proof, outcome) end
             val _ = print_d (fn () => "Preparing problem for " ^

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