src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

      max_new_mono_instances : int option,
      isar_proofs : bool,
      isar_shrink : real,
      slice : bool,
      minimize : bool option,
-     timeout : Time.time,
-     preplay_timeout : Time.time,
+     timeout : Time.time option,
+     preplay_timeout : Time.time option,
      expect : string}
 
   type relevance_fudge =
     {local_const_multiplier : real,
      worse_irrel_freq : real,

    max_new_mono_instances : int option,
    isar_proofs : bool,
    isar_shrink : real,
    slice : bool,
    minimize : bool option,
-   timeout : Time.time,
-   preplay_timeout : Time.time,
+   timeout : Time.time option,
+   preplay_timeout : Time.time option,
    expect : string}
 
 type relevance_fudge =
   {local_const_multiplier : real,
    worse_irrel_freq : real,

 (* 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 TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
+  in time_limit timeout (try (Seq.pull o full_tac)) goal end
 
 fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
     metis_tac [type_enc] lam_trans
   | tac_for_reconstructor SMT = SMT_Solver.smt_tac
 

           (if keep_chained then is_fact_chained else K false))
 
 fun play_one_line_proof mode debug verbose timeout pairs state i preferred
                         reconstrs =
   let
-    val _ =
-      if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
-        Output.urgent_message "Preplaying proof..."
-      else
-        ()
-    val ths = pairs |> sort_wrt (fst o fst) |> map snd
     fun get_preferred reconstrs =
       if member (op =) reconstrs preferred then preferred
       else List.last reconstrs
-    fun play [] [] = Failed_to_Play (get_preferred reconstrs)
-      | play timed_outs [] =
-        Trust_Playable (get_preferred timed_outs, SOME timeout)
-      | play timed_out (reconstr :: reconstrs) =
-        let
-          val _ =
-            if verbose then
-              "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^
-              string_from_time timeout ^ "..."
-              |> Output.urgent_message
-            else
-              ()
-          val timer = Timer.startRealTimer ()
-        in
-          case timed_reconstructor reconstr debug timeout ths state i of
-            SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
-          | _ => play timed_out reconstrs
-        end
-        handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
   in
-    if timeout = Time.zeroTime then
+    if timeout = SOME Time.zeroTime then
       Trust_Playable (get_preferred reconstrs, NONE)
     else
-      play [] reconstrs
+      let
+        val _ =
+          if mode = Minimize then Output.urgent_message "Preplaying proof..."
+          else ()
+        val ths = pairs |> sort_wrt (fst o fst) |> map snd
+        fun play [] [] = Failed_to_Play (get_preferred reconstrs)
+          | play timed_outs [] =
+            Trust_Playable (get_preferred timed_outs, timeout)
+          | play timed_out (reconstr :: reconstrs) =
+            let
+              val _ =
+                if verbose then
+                  "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^
+                  (case timeout of
+                     SOME timeout => " for " ^ string_from_time timeout
+                   | NONE => "") ^ "..."
+                  |> Output.urgent_message
+                else
+                  ()
+              val timer = Timer.startRealTimer ()
+            in
+              case timed_reconstructor reconstr debug timeout ths state i of
+                SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+              | _ => play timed_out reconstrs
+            end
+            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+      in play [] reconstrs end
   end
 
 
 (* generic TPTP-based ATPs *)
 

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

                                        readable_names true hyp_ts concl_t
             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 = debug orelse isar_proofs
-            val args = arguments ctxt full_proof extra slice_timeout
+            val args = arguments ctxt full_proof extra
+                                 (slice_timeout |> the_default one_day)
                                  (ord, ord_info, sel_weights)
             val command =
               "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
               File.shell_path prob_path ^ ")"
               |> enclose "TIMEFORMAT='%3R'; { time " " ; }"

               atp_problem
               |> lines_for_atp_problem format ord ord_info
               |> cons ("% " ^ command ^ "\n")
               |> File.write_list prob_path
             val ((output, run_time), (atp_proof, outcome)) =
-              TimeLimit.timeLimit generous_slice_timeout
-                                  Isabelle_System.bash_output command
+              time_limit generous_slice_timeout Isabelle_System.bash_output
+                         command
               |>> (if overlord then
                      prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
                    else
                      I)
               |> fst |> split_time

                                                          known_failures output
                       |>> atp_proof_from_tstplike_proof atp_problem
                       handle UNRECOGNIZED_ATP_PROOF () =>
                              ([], SOME ProofIncomplete)))
               handle TimeLimit.TimeOut =>
-                     (("", slice_timeout), ([], SOME TimedOut))
+                     (("", the 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

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

         val state =
           state |> Proof.map_context
                        (repair_monomorph_context max_mono_iters
                             default_max_mono_iters max_new_mono_instances
                             default_max_new_mono_instances)
-        val ms = timeout |> Time.toMilliseconds
         val slice_timeout =
-          if slice < max_slices then
-            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
+          if slice < max_slices andalso timeout <> NONE then
+            let val ms = timeout |> the |> Time.toMilliseconds 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
+            end
           else
             timeout
         val num_facts = length facts
         val _ =
           if debug then
             quote name ^ " slice " ^ string_of_int slice ^ " with " ^
-            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
-            string_from_time slice_timeout ^ "..."
+            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+            (case slice_timeout of
+               SOME timeout => " for " ^ string_from_time timeout
+             | NONE => "") ^ "..."
             |> Output.urgent_message
           else
             ()
         val birth = Timer.checkRealTimer timer
         val _ =
           if debug then Output.urgent_message "Invoking SMT solver..." else ()
         val state_facts = these (try (#facts o Proof.goal) state)
         val (outcome, used_facts) =
           SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
-          |> SMT_Solver.smt_filter_apply slice_timeout
+          |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
           |> (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 = Time.- (timeout, Timer.checkRealTimer timer)
+        val timeout =
+          Option.map
+              (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+              timeout
       in
         if too_many_facts_perhaps andalso slice < max_slices andalso
-           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
+           num_facts > 0 andalso
+           (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
           let
             val new_num_facts =
               Real.ceil (Config.get ctxt smt_slice_fact_frac
                          * Real.fromInt num_facts)
             val _ =