src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

   val someN : string
   val noneN : string
   val timeoutN : string
   val unknownN : string
   val string_of_factss : (string * fact list) list -> string
-  val run_sledgehammer :
-    params -> mode -> (string -> unit) option -> int -> fact_override
-    -> ((string * string list) list -> string -> minimize_command)
-    -> Proof.state -> bool * (string * Proof.state)
+  val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
+    ((string * string list) list -> string -> minimize_command) -> Proof.state ->
+    bool * (string * Proof.state)
 end;
 
 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
 struct
 

       "") ^
    " 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))))
 
-fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...})
-        mode output_result minimize_command only learn
-        {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
+fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
+    output_result minimize_command only learn
+    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
   let
     val ctxt = Proof.context_of state
 
-    val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
+    val hard_timeout = time_mult 3.0 timeout
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
     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

           else
             warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
       in (outcome_code, message) end
   in
     if mode = Auto_Try then
-      let val (outcome_code, message) = time_limit timeout go () in
+      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
         (outcome_code,
          state
          |> outcome_code = someN
             ? Proof.goal_message (fn () =>
                   Pretty.mark Markup.information (Pretty.str (message ()))))