src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

      isar_proofs : bool option,
      isar_compress : real,
      isar_try0 : bool,
      slice : bool,
      minimize : bool option,
-     timeout : Time.time option,
-     preplay_timeout : Time.time option,
+     timeout : Time.time,
+     preplay_timeout : Time.time,
      expect : string}
 
   type prover_problem =
     {comment : string,
      state : Proof.state,

    isar_proofs : bool option,
    isar_compress : real,
    isar_try0 : bool,
    slice : bool,
    minimize : bool option,
-   timeout : Time.time option,
-   preplay_timeout : Time.time option,
+   timeout : Time.time,
+   preplay_timeout : Time.time,
    expect : string}
 
 type prover_problem =
   {comment : string,
    state : Proof.state,

 (* based on "Mirabelle.can_apply" and generalized *)
 fun timed_apply timeout tac state i =
   let
     val {context = ctxt, facts, goal} = Proof.goal state
     val full_tac = Method.insert_tac facts i THEN tac ctxt i
-  in time_limit timeout (try (Seq.pull o full_tac)) goal end
+  in
+    TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
+  end
 
 fun tac_of_reconstructor (Metis (type_enc, lam_trans)) =
     metis_tac [type_enc] lam_trans
   | tac_of_reconstructor SMT = SMT_Solver.smt_tac
 

   let
     fun get_preferred reconstrs =
       if member (op =) reconstrs preferred then preferred
       else List.last reconstrs
   in
-    if timeout = SOME Time.zeroTime then
+    if timeout = Time.zeroTime then
       Play_Timed_Out (get_preferred reconstrs, Time.zeroTime)
     else
       let
         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
         val ths = pairs |> sort_wrt (fst o fst) |> map snd
         fun play [] [] = Play_Failed (get_preferred reconstrs)
-          | play timed_outs [] =
-            Play_Timed_Out (get_preferred timed_outs, timeout |> the_default Time.zeroTime (* wrong *))
+          | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout)
           | play timed_out (reconstr :: reconstrs) =
             let
               val _ =
                 if verbose then
-                  "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
-                  (case timeout of
-                     SOME timeout => " for " ^ string_of_time timeout
-                   | NONE => "") ^ "..."
-                  |> Output.urgent_message
+                  Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
+                    "\" for " ^ string_of_time timeout ^ "...")
                 else
                   ()
               val timer = Timer.startRealTimer ()
             in
               case timed_reconstructor reconstr debug timeout ths state i of

             val type_enc =
               type_enc |> choose_type_enc strictness best_type_enc format
             val sound = is_type_enc_sound type_enc
             val real_ms = Real.fromInt o Time.toMilliseconds
             val slice_timeout =
-              case time_left of
-                SOME time_left =>
-                ((real_ms time_left
-                  |> (if slice < num_actual_slices - 1 then
-                        curry Real.min (time_frac * real_ms (the timeout))
-                      else
-                        I))
-                 * 0.001)
-                |> seconds |> SOME
-              | NONE => NONE
+              (real_ms time_left
+               |> (if slice < num_actual_slices - 1 then
+                     curry Real.min (time_frac * real_ms timeout)
+                   else
+                     I))
+              * 0.001
+              |> seconds
             val generous_slice_timeout =
-              if mode = MaSh then NONE
-              else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
+              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
             val _ =
               if debug then
                 quote name ^ " slice #" ^ string_of_int (slice + 1) ^
                 " with " ^ string_of_int num_facts ^ " fact" ^
-                plural_s num_facts ^
-                (case slice_timeout of
-                   SOME timeout => " for " ^ string_of_time timeout
-                 | NONE => "") ^ "..."
+                plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
                 |> Output.urgent_message
               else
                 ()
             val readable_names = not (Config.get ctxt atp_full_names)
             val lam_trans =

             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem
             val ord = effective_term_order ctxt name
             val full_proof = isar_proofs |> the_default (mode = Minimize)
             val args =
-              arguments ctxt full_proof extra (slice_timeout |> the_default one_day)
-                        (File.shell_path prob_path) (ord, ord_info, sel_weights)
+              arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
+                (ord, ord_info, sel_weights)
             val command =
               "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
               |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
             val _ =
               atp_problem
               |> lines_of_atp_problem format ord ord_info
               |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
               |> File.write_list prob_path
             val ((output, run_time), (atp_proof, outcome)) =
-              time_limit generous_slice_timeout Isabelle_System.bash_output command
+              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
               |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
               |> fst |> split_time
               |> (fn accum as (output, _) =>
                      (accum,
                       extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
                       |>> atp_proof_of_tstplike_proof atp_problem
                       handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
-              handle TimeLimit.TimeOut => (("", the slice_timeout), ([], SOME TimedOut))
+              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
             val outcome =
               case outcome of
                 NONE =>
                 (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
                       |> Option.map (sort string_ord) of

           end
         val timer = Timer.startRealTimer ()
         fun maybe_run_slice slice
                 (result as (cache, (_, run_time0, _, _, SOME _))) =
             let
-              val time_left =
-                Option.map
-                    (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
-                    timeout
+              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
             in
-              if time_left <> NONE andalso
-                 Time.<= (the time_left, Time.zeroTime) then
+              if Time.<= (time_left, Time.zeroTime) then
                 result
               else
                 run_slice time_left cache slice
                 |> (fn (cache, (output, run_time, used_from, atp_proof,
                                 outcome)) =>

     fun do_slice timeout slice outcome0 time_so_far
                  (weighted_factss as (fact_filter, weighted_facts) :: _) =
       let
         val timer = Timer.startRealTimer ()
         val slice_timeout =
-          if slice < max_slices andalso timeout <> NONE then
-            let val ms = timeout |> the |> Time.toMilliseconds in
+          if slice < max_slices then
+            let val ms = Time.toMilliseconds timeout in
               Int.min (ms,
                   Int.max (1000 * Config.get ctxt smt_slice_min_secs,
                       Real.ceil (Config.get ctxt smt_slice_time_frac
                                  * Real.fromInt ms)))
-              |> Time.fromMilliseconds |> SOME
+              |> Time.fromMilliseconds
             end
           else
             timeout
         val num_facts = length weighted_facts
         val _ =
           if debug then
-            quote name ^ " slice " ^ string_of_int slice ^ " with " ^
-            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
-            (case slice_timeout of
-               SOME timeout => " for " ^ string_of_time timeout
-             | NONE => "") ^ "..."
+            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
+            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
             |> Output.urgent_message
           else
             ()
         val birth = Timer.checkRealTimer timer
         val _ =
           if debug then Output.urgent_message "Invoking SMT solver..." else ()
         val (outcome, used_facts) =
           SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
-          |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
+          |> SMT_Solver.smt_filter_apply slice_timeout
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then
                           reraise exn
                         else
                           (ML_Compiler.exn_message exn

           | SOME (SMT_Failure.Counterexample _) => false
           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
           | SOME SMT_Failure.Out_Of_Memory => true
           | SOME (SMT_Failure.Other_Failure _) => true
-        val timeout =
-          Option.map
-              (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
-              timeout
+        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
       in
-        if too_many_facts_perhaps andalso slice < max_slices andalso
-           num_facts > 0 andalso
-           (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
+        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
+           Time.> (timeout, Time.zeroTime) then
           let
             val new_num_facts =
-              Real.ceil (Config.get ctxt smt_slice_fact_frac
-                         * Real.fromInt num_facts)
+              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
             val weighted_factss as (new_fact_filter, _) :: _ =
               weighted_factss
               |> rotate_one
               |> app_hd (apsnd (take new_num_facts))
             val show_filter = fact_filter <> new_fact_filter