tuned signature -- clarified modules;
authorwenzelm
Sat Mar 05 17:01:45 2016 +0100 (2016-03-05)
changeset 62519a564458f94db
parent 62518 b8efcc9edd7b
child 62520 2382876c238b
tuned signature -- clarified modules;
NEWS
src/HOL/Library/Old_SMT/old_smt_config.ML
src/HOL/Library/refute.ML
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mirabelle/Tools/mirabelle_arith.ML
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
src/HOL/Mirabelle/Tools/mirabelle_refute.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_try0.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/atp_theory_export.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/z3_replay.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/try0.ML
src/Pure/Concurrent/time_limit.ML
src/Pure/Concurrent/timeout.ML
src/Pure/Isar/runtime.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Tools/quickcheck.ML
src/Tools/try.ML
     1.1 --- a/NEWS	Sat Mar 05 13:57:25 2016 +0100
     1.2 +++ b/NEWS	Sat Mar 05 17:01:45 2016 +0100
     1.3 @@ -197,6 +197,10 @@
     1.4  balanced blocks of Local_Theory.open_target versus
     1.5  Local_Theory.close_target instead. Rare INCOMPATIBILITY.
     1.6  
     1.7 +* Structure TimeLimit (originally from the SML/NJ library) has been
     1.8 +replaced by structure Timeout, with slightly different signature.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** System ***
    1.13  
     2.1 --- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Sat Mar 05 13:57:25 2016 +0100
     2.2 +++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Sat Mar 05 17:01:45 2016 +0100
     2.3 @@ -177,8 +177,8 @@
     2.4  (* tools *)
     2.5  
     2.6  fun with_timeout ctxt f x =
     2.7 -  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
     2.8 -  handle TimeLimit.TimeOut => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
     2.9 +  Timeout.apply (seconds (Config.get ctxt timeout)) f x
    2.10 +    handle Timeout.TIMEOUT _ => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
    2.11  
    2.12  
    2.13  (* certificates *)
     3.1 --- a/src/HOL/Library/refute.ML	Sat Mar 05 13:57:25 2016 +0100
     3.2 +++ b/src/HOL/Library/refute.ML	Sat Mar 05 17:01:45 2016 +0100
     3.3 @@ -1031,7 +1031,7 @@
     3.4            let
     3.5              val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
     3.6              val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
     3.7 -                    orelse raise TimeLimit.TimeOut
     3.8 +                    orelse raise Timeout.TIMEOUT (Time.fromMilliseconds msecs_spent)
     3.9              val init_model = (universe, [])
    3.10              val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
    3.11                bounds = [], wellformed = True}
    3.12 @@ -1115,9 +1115,9 @@
    3.13        ^ (if negate then "refutes" else "satisfies") ^ ": "
    3.14        ^ Syntax.string_of_term ctxt t);
    3.15      if maxtime > 0 then (
    3.16 -      TimeLimit.timeLimit (Time.fromSeconds maxtime)
    3.17 +      Timeout.apply (Time.fromSeconds maxtime)
    3.18          wrapper ()
    3.19 -      handle TimeLimit.TimeOut =>
    3.20 +      handle Timeout.TIMEOUT _ =>
    3.21          (writeln ("Search terminated, time limit (" ^
    3.22              string_of_int maxtime
    3.23              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 05 13:57:25 2016 +0100
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 05 17:01:45 2016 +0100
     4.3 @@ -156,7 +156,7 @@
     4.4      val {context = ctxt, facts, goal} = Proof.goal st
     4.5      val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
     4.6    in
     4.7 -    (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
     4.8 +    (case try (Timeout.apply time (Seq.pull o full_tac)) goal of
     4.9        SOME (SOME _) => true
    4.10      | _ => false)
    4.11    end
     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Mar 05 13:57:25 2016 +0100
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Mar 05 17:01:45 2016 +0100
     5.3 @@ -14,7 +14,7 @@
     5.4    if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
     5.5    then log (arith_tag id ^ "succeeded")
     5.6    else ()
     5.7 -  handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
     5.8 +  handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout")
     5.9  
    5.10  fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
    5.11  
     6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Mar 05 13:57:25 2016 +0100
     6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Mar 05 17:01:45 2016 +0100
     6.3 @@ -27,7 +27,7 @@
     6.4      |> add_info
     6.5      |> log
     6.6    end
     6.7 -  handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
     6.8 +  handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout")
     6.9         | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
    6.10  
    6.11  fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
     7.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Mar 05 13:57:25 2016 +0100
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Mar 05 17:01:45 2016 +0100
     7.3 @@ -15,11 +15,11 @@
     7.4      val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     7.5      val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
     7.6    in
     7.7 -    (case TimeLimit.timeLimit timeout quickcheck pre of
     7.8 +    (case Timeout.apply timeout quickcheck pre of
     7.9        NONE => log (qc_tag id ^ "no counterexample")
    7.10      | SOME _ => log (qc_tag id ^ "counterexample found"))
    7.11    end
    7.12 -  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
    7.13 +  handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout")
    7.14         | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
    7.15  
    7.16  fun invoke args =
     8.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Mar 05 13:57:25 2016 +0100
     8.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Mar 05 17:01:45 2016 +0100
     8.3 @@ -14,7 +14,7 @@
     8.4      val thm = #goal (Proof.raw_goal st)
     8.5  
     8.6      val refute = Refute.refute_goal thy args thm
     8.7 -    val _ = TimeLimit.timeLimit timeout refute subgoal
     8.8 +    val _ = Timeout.apply timeout refute subgoal
     8.9    in
    8.10      val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
    8.11      val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
     9.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Mar 05 13:57:25 2016 +0100
     9.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Mar 05 17:01:45 2016 +0100
     9.3 @@ -404,7 +404,7 @@
     9.4      val time_limit =
     9.5        (case hard_timeout of
     9.6          NONE => I
     9.7 -      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     9.8 +      | SOME secs => Timeout.apply (Time.fromSeconds secs))
     9.9      fun failed failure =
    9.10        ({outcome = SOME failure, used_facts = [], used_from = [],
    9.11          preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime,
    9.12 @@ -434,7 +434,7 @@
    9.13            {comment = "", state = st', goal = goal, subgoal = i,
    9.14             subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
    9.15        in prover params problem end)) ()
    9.16 -      handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
    9.17 +      handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
    9.18             | Fail "inappropriate" => failed ATP_Proof.Inappropriate
    9.19      val time_prover = run_time |> Time.toMilliseconds
    9.20      val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts
    9.21 @@ -590,7 +590,7 @@
    9.22            "succeeded (" ^ string_of_int t ^ ")")
    9.23      fun timed_method named_thms =
    9.24        (with_time (Mirabelle.cpu_time apply_method named_thms), true)
    9.25 -      handle TimeLimit.TimeOut => (change_data id inc_proof_method_timeout; ("timeout", false))
    9.26 +      handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false))
    9.27             | ERROR msg => ("error: " ^ msg, false)
    9.28  
    9.29      val _ = log separator
    9.30 @@ -628,7 +628,7 @@
    9.31              if AList.lookup (op =) args check_trivialK |> the_default trivial_default
    9.32                              |> Markup.parse_bool then
    9.33                Try0.try0 (SOME try_timeout) ([], [], [], []) pre
    9.34 -              handle TimeLimit.TimeOut => false
    9.35 +              handle Timeout.TIMEOUT _ => false
    9.36              else false
    9.37            fun apply_method () =
    9.38              (Mirabelle.catch_result (proof_method_tag meth) false
    10.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Sat Mar 05 13:57:25 2016 +0100
    10.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Sat Mar 05 17:01:45 2016 +0100
    10.3 @@ -13,10 +13,10 @@
    10.4  fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
    10.5  
    10.6  fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
    10.7 -  if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
    10.8 +  if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
    10.9    then log (try0_tag id ^ "succeeded")
   10.10    else ()
   10.11 -  handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")
   10.12 +  handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout")
   10.13  
   10.14  fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done)
   10.15  
    11.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 05 13:57:25 2016 +0100
    11.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 05 17:01:45 2016 +0100
    11.3 @@ -110,7 +110,7 @@
    11.4  (** quickcheck **)
    11.5  
    11.6  fun invoke_quickcheck change_options thy t =
    11.7 -  TimeLimit.timeLimit (seconds 30.0)
    11.8 +  Timeout.apply (seconds 30.0)
    11.9        (fn _ =>
   11.10            let
   11.11              val ctxt' = change_options (Proof_Context.init_global thy)
   11.12 @@ -123,7 +123,7 @@
   11.13                NONE => (NoCex, Quickcheck.timings_of result)
   11.14              | SOME _ => (GenuineCex, Quickcheck.timings_of result)
   11.15            end) ()
   11.16 -  handle TimeLimit.TimeOut =>
   11.17 +  handle Timeout.TIMEOUT _ =>
   11.18           (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
   11.19  
   11.20  fun quickcheck_mtd change_options quickcheck_generator =
   11.21 @@ -314,7 +314,7 @@
   11.22    let
   11.23      val ctxt = Proof_Context.init_global thy
   11.24    in
   11.25 -    can (TimeLimit.timeLimit (seconds 30.0)
   11.26 +    can (Timeout.apply (seconds 30.0)
   11.27        (Quickcheck.test_terms
   11.28          ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
   11.29            Config.put Quickcheck.finite_types true #>
    12.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Mar 05 13:57:25 2016 +0100
    12.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Mar 05 17:01:45 2016 +0100
    12.3 @@ -162,14 +162,14 @@
    12.4        Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
    12.5      val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
    12.6      val (mono_free_Ts, nonmono_free_Ts) =
    12.7 -      TimeLimit.timeLimit mono_timeout
    12.8 +      Timeout.apply mono_timeout
    12.9            (List.partition is_type_actually_monotonic) free_Ts
   12.10    in
   12.11      if not (null mono_free_Ts) then "MONO"
   12.12      else if not (null nonmono_free_Ts) then "NONMONO"
   12.13      else "NIX"
   12.14    end
   12.15 -  handle TimeLimit.TimeOut => "TIMEOUT"
   12.16 +  handle Timeout.TIMEOUT _ => "TIMEOUT"
   12.17         | NOT_SUPPORTED _ => "UNSUP"
   12.18         | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
   12.19  
   12.20 @@ -182,11 +182,11 @@
   12.21          val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
   12.22          val neg_t = Logic.mk_implies (t, @{prop False})
   12.23          val (nondef_ts, def_ts, _, _, _, _) =
   12.24 -          TimeLimit.timeLimit preproc_timeout (preprocess_formulas hol_ctxt [])
   12.25 +          Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
   12.26                                neg_t
   12.27          val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
   12.28        in File.append path (res ^ "\n"); writeln res end
   12.29 -      handle TimeLimit.TimeOut => ()
   12.30 +      handle Timeout.TIMEOUT _ => ()
   12.31    in thy |> theorems_of |> List.app check_theorem end
   12.32  *}
   12.33  
    13.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Sat Mar 05 13:57:25 2016 +0100
    13.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Sat Mar 05 17:01:45 2016 +0100
    13.3 @@ -35,7 +35,7 @@
    13.4  ML {*
    13.5    (*default timeout is 1 min*)
    13.6    fun interpret timeout file thy =
    13.7 -    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    13.8 +    Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    13.9       (TPTP_Interpret.interpret_file
   13.10         false
   13.11         [Path.explode "$TPTP"]
    14.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sat Mar 05 13:57:25 2016 +0100
    14.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sat Mar 05 17:01:45 2016 +0100
    14.3 @@ -1060,7 +1060,7 @@
    14.4            tactic takes too long*)
    14.5          val try_make_step =
    14.6            (*FIXME const timeout*)
    14.7 -          (* TimeLimit.timeLimit (Time.fromSeconds 5) *)
    14.8 +          (* Timeout.apply (Time.fromSeconds 5) *)
    14.9            (fn ctxt' =>
   14.10               let
   14.11                 fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
    15.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sat Mar 05 13:57:25 2016 +0100
    15.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sat Mar 05 17:01:45 2016 +0100
    15.3 @@ -634,7 +634,7 @@
    15.4      let
    15.5        val timer = Timer.startRealTimer ()
    15.6      in
    15.7 -      TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    15.8 +      Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    15.9         (test_partial_reconstruction thy
   15.10          #> light_output ? erase_inference_fmlas
   15.11          #> @{make_string} (* FIXME *)
   15.12 @@ -662,7 +662,7 @@
   15.13          |> Path.implode
   15.14          |> TPTP_Problem_Name.Nonstandard
   15.15      in
   15.16 -      TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
   15.17 +      Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
   15.18         (fn prob_name =>
   15.19          (can
   15.20            (TPTP_Reconstruct.reconstruct ctxt (fn prob_name =>
    16.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Sat Mar 05 13:57:25 2016 +0100
    16.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Sat Mar 05 17:01:45 2016 +0100
    16.3 @@ -137,10 +137,8 @@
    16.4    let
    16.5      val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
    16.6      val result =
    16.7 -      TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
    16.8 -      handle
    16.9 -        TimeLimit.TimeOut => NONE
   16.10 -      | ERROR _ => NONE
   16.11 +      Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
   16.12 +        handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
   16.13    in
   16.14      (case result of
   16.15        NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    17.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Sat Mar 05 13:57:25 2016 +0100
    17.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Mar 05 17:01:45 2016 +0100
    17.3 @@ -63,11 +63,11 @@
    17.4        arguments ctxt false "" atp_timeout (File.shell_path prob_file)
    17.5                  (ord, K [], K [])
    17.6      val outcome =
    17.7 -      TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command
    17.8 +      Timeout.apply atp_timeout Isabelle_System.bash_output command
    17.9        |> fst
   17.10        |> extract_tstplike_proof_and_outcome false proof_delims known_failures
   17.11        |> snd
   17.12 -      handle TimeLimit.TimeOut => SOME TimedOut
   17.13 +      handle Timeout.TIMEOUT _ => SOME TimedOut
   17.14      val _ =
   17.15        tracing ("Ran ATP: " ^
   17.16                 (case outcome of
    18.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Mar 05 13:57:25 2016 +0100
    18.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Mar 05 17:01:45 2016 +0100
    18.3 @@ -633,7 +633,7 @@
    18.4  val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
    18.5  
    18.6  fun get_remote_systems () =
    18.7 -  TimeLimit.timeLimit (seconds 10.0) (fn () =>
    18.8 +  Timeout.apply (seconds 10.0) (fn () =>
    18.9      (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   18.10        (output, 0) => split_lines output
   18.11      | (output, _) =>
   18.12 @@ -641,7 +641,7 @@
   18.13           (case extract_known_atp_failure known_perl_failures output of
   18.14             SOME failure => string_of_atp_failure failure
   18.15           | NONE => trim_line output ^ "."); []))) ()
   18.16 -  handle TimeLimit.TimeOut => []
   18.17 +  handle Timeout.TIMEOUT _ => []
   18.18  
   18.19  fun find_remote_system name [] systems =
   18.20      find_first (String.isPrefix (name ^ "---")) systems
    19.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Mar 05 13:57:25 2016 +0100
    19.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Mar 05 17:01:45 2016 +0100
    19.3 @@ -211,6 +211,7 @@
    19.4  fun pick_them_nits_in_term deadline state (params : params) mode i n step
    19.5                             subst def_assm_ts nondef_assm_ts orig_t =
    19.6    let
    19.7 +    val time_start = Time.now ()
    19.8      val timer = Timer.startRealTimer ()
    19.9      val thy = Proof.theory_of state
   19.10      val ctxt = Proof.context_of state
   19.11 @@ -248,10 +249,11 @@
   19.12      val print_v = pprint_v o K o plazy
   19.13  
   19.14      fun check_deadline () =
   19.15 -      if Time.compare (Time.now (), deadline) <> LESS then
   19.16 -        raise TimeLimit.TimeOut
   19.17 -      else
   19.18 -        ()
   19.19 +      let val t = Time.now () in
   19.20 +        if Time.compare (t, deadline) <> LESS
   19.21 +        then raise Timeout.TIMEOUT (Time.- (t, time_start))
   19.22 +        else ()
   19.23 +      end
   19.24  
   19.25      val (def_assm_ts, nondef_assm_ts) =
   19.26        if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
   19.27 @@ -376,9 +378,9 @@
   19.28         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
   19.29        is_number_type ctxt T orelse is_bit_type T
   19.30      fun is_type_actually_monotonic T =
   19.31 -      TimeLimit.timeLimit tac_timeout (formulas_monotonic hol_ctxt binarize T)
   19.32 +      Timeout.apply tac_timeout (formulas_monotonic hol_ctxt binarize T)
   19.33                            (nondef_ts, def_ts)
   19.34 -      handle TimeLimit.TimeOut => false
   19.35 +        handle Timeout.TIMEOUT _ => false
   19.36      fun is_type_kind_of_monotonic T =
   19.37        case triple_lookup (type_match thy) monos T of
   19.38          SOME (SOME false) => false
   19.39 @@ -806,7 +808,7 @@
   19.40                  end
   19.41              end
   19.42            | KK.TimedOut unsat_js =>
   19.43 -            (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
   19.44 +            (update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime)
   19.45            | KK.Error (s, unsat_js) =>
   19.46              (update_checked_problems problems unsat_js;
   19.47               print_v (K ("Kodkod error: " ^ s ^ "."));
   19.48 @@ -958,7 +960,7 @@
   19.49      val outcome_code =
   19.50        run_batches 0 (length batches) batches
   19.51                    (false, max_potential, max_genuine, 0)
   19.52 -      handle TimeLimit.TimeOut =>
   19.53 +      handle Timeout.TIMEOUT _ =>
   19.54               (print_nt (fn () => excipit "ran out of time after checking");
   19.55                if !met_potential > 0 then potentialN else unknownN)
   19.56      val _ = print_v (fn () =>
   19.57 @@ -986,7 +988,7 @@
   19.58          val unknown_outcome = (unknownN, [])
   19.59          val deadline = Time.+ (Time.now (), timeout)
   19.60          val outcome as (outcome_code, _) =
   19.61 -          TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
   19.62 +          Timeout.apply (Time.+ (timeout, timeout_bonus))
   19.63                (pick_them_nits_in_term deadline state params mode i n step subst
   19.64                                        def_assm_ts nondef_assm_ts) orig_t
   19.65            handle TOO_LARGE (_, details) =>
   19.66 @@ -999,7 +1001,7 @@
   19.67                   (print_t "% SZS status GaveUp";
   19.68                    print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
   19.69                    unknown_outcome)
   19.70 -               | TimeLimit.TimeOut =>
   19.71 +               | Timeout.TIMEOUT _ =>
   19.72                   (print_t "% SZS status TimedOut";
   19.73                    print_nt "Nitpick ran out of time."; unknown_outcome)
   19.74        in
    20.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Mar 05 13:57:25 2016 +0100
    20.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Mar 05 17:01:45 2016 +0100
    20.3 @@ -577,18 +577,18 @@
    20.4            |> List.partition (member (op =) ["dptsat", "cdclite"] o fst)
    20.5          val res =
    20.6            if null nonml_solvers then
    20.7 -            TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop
    20.8 +            Timeout.apply tac_timeout (snd (hd ml_solvers)) prop
    20.9            else
   20.10 -            TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop
   20.11 -            handle TimeLimit.TimeOut =>
   20.12 -                   TimeLimit.timeLimit tac_timeout
   20.13 +            Timeout.apply ml_solver_timeout (snd (hd ml_solvers)) prop
   20.14 +            handle Timeout.TIMEOUT _ =>
   20.15 +                   Timeout.apply tac_timeout
   20.16                                         (SAT_Solver.invoke_solver "auto") prop
   20.17        in
   20.18          case res of
   20.19            SAT_Solver.SATISFIABLE assigns => do_assigns assigns
   20.20          | _ => (trace_msg (K "*** Unsolvable"); NONE)
   20.21        end
   20.22 -      handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE)
   20.23 +      handle Timeout.TIMEOUT _ => (trace_msg (K "*** Timed out"); NONE)
   20.24    end
   20.25  
   20.26  type mcontext =
    21.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Mar 05 13:57:25 2016 +0100
    21.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Mar 05 17:01:45 2016 +0100
    21.3 @@ -273,7 +273,7 @@
    21.4  val eta_expand = ATP_Util.eta_expand
    21.5  
    21.6  fun DETERM_TIMEOUT delay tac st =
    21.7 -  Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ()))
    21.8 +  Seq.of_list (the_list (Timeout.apply delay (fn () => SINGLE tac st) ()))
    21.9  
   21.10  val indent_size = 2
   21.11  
    22.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Mar 05 13:57:25 2016 +0100
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Mar 05 17:01:45 2016 +0100
    22.3 @@ -882,7 +882,7 @@
    22.4      val args' = map (rename_vars_term renaming) args
    22.5      val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
    22.6      val _ = tracing ("Generated prolog program:\n" ^ prog)
    22.7 -    val solution = TimeLimit.timeLimit timeout (fn prog =>
    22.8 +    val solution = Timeout.apply timeout (fn prog =>
    22.9        Isabelle_System.with_tmp_file "prolog_file" "" (fn prolog_file =>
   22.10          (File.write prolog_file prog; invoke system prolog_file))) prog
   22.11      val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
    23.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Mar 05 13:57:25 2016 +0100
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Mar 05 17:01:45 2016 +0100
    23.3 @@ -1890,7 +1890,7 @@
    23.4            let
    23.5              val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
    23.6            in
    23.7 -            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
    23.8 +            rpair NONE (Timeout.apply time_limit (fn () => fst (Limited_Sequence.yieldn k
    23.9                (Code_Runtime.dynamic_value_strict
   23.10                  (get_dseq_random_result, put_dseq_random_result,
   23.11                    "Predicate_Compile_Core.put_dseq_random_result")
   23.12 @@ -1902,7 +1902,7 @@
   23.13                depth true)) ())
   23.14            end
   23.15        | DSeq =>
   23.16 -          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
   23.17 +          rpair NONE (Timeout.apply time_limit (fn () => fst (Limited_Sequence.yieldn k
   23.18              (Code_Runtime.dynamic_value_strict
   23.19                (get_dseq_result, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
   23.20                ctxt NONE Limited_Sequence.map t' [])
   23.21 @@ -1911,7 +1911,7 @@
   23.22            let
   23.23              val depth = Code_Numeral.natural_of_integer (the_single arguments)
   23.24            in
   23.25 -            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
   23.26 +            rpair NONE (Timeout.apply time_limit (fn () => fst (Lazy_Sequence.yieldn k
   23.27                (Code_Runtime.dynamic_value_strict
   23.28                  (get_new_dseq_result, put_new_dseq_result,
   23.29                    "Predicate_Compile_Core.put_new_dseq_result")
   23.30 @@ -1925,7 +1925,7 @@
   23.31            in
   23.32              if stats then
   23.33                apsnd (SOME o accumulate o map Code_Numeral.integer_of_natural)
   23.34 -              (split_list (TimeLimit.timeLimit time_limit
   23.35 +              (split_list (Timeout.apply time_limit
   23.36                (fn () => fst (Lazy_Sequence.yieldn k
   23.37                  (Code_Runtime.dynamic_value_strict
   23.38                    (get_lseq_random_stats_result, put_lseq_random_stats_result,
   23.39 @@ -1936,7 +1936,7 @@
   23.40                      |> Lazy_Sequence.map (apfst proc))
   23.41                      t' [] nrandom size seed depth))) ()))
   23.42              else rpair NONE
   23.43 -              (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
   23.44 +              (Timeout.apply time_limit (fn () => fst (Lazy_Sequence.yieldn k
   23.45                  (Code_Runtime.dynamic_value_strict
   23.46                    (get_lseq_random_result, put_lseq_random_result,
   23.47                      "Predicate_Compile_Core.put_lseq_random_result")
   23.48 @@ -1947,11 +1947,11 @@
   23.49                        t' [] nrandom size seed depth))) ())
   23.50            end
   23.51        | _ =>
   23.52 -          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
   23.53 +          rpair NONE (Timeout.apply time_limit (fn () => fst (Predicate.yieldn k
   23.54              (Code_Runtime.dynamic_value_strict
   23.55                (get_pred_result, put_pred_result, "Predicate_Compile_Core.put_pred_result")
   23.56                ctxt NONE Predicate.map t' []))) ()))
   23.57 -     handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
   23.58 +     handle Timeout.TIMEOUT _ => error "Reached timeout during execution of values"
   23.59    in ((T, ts), statistics) end;
   23.60  
   23.61  fun values param_user_modes ((raw_expected, stats), comp_options) k t_compr ctxt =
    24.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Sat Mar 05 13:57:25 2016 +0100
    24.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Sat Mar 05 17:01:45 2016 +0100
    24.3 @@ -196,8 +196,8 @@
    24.4  (* tools *)
    24.5  
    24.6  fun with_time_limit ctxt timeout_config f x =
    24.7 -  TimeLimit.timeLimit (seconds (Config.get ctxt timeout_config)) f x
    24.8 -  handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
    24.9 +  Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
   24.10 +    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
   24.11  
   24.12  fun with_timeout ctxt = with_time_limit ctxt timeout
   24.13  
    25.1 --- a/src/HOL/Tools/SMT/z3_replay.ML	Sat Mar 05 13:57:25 2016 +0100
    25.2 +++ b/src/HOL/Tools/SMT/z3_replay.ML	Sat Mar 05 17:01:45 2016 +0100
    25.3 @@ -72,7 +72,7 @@
    25.4      val replay = Timing.timing (replay_thm ctxt assumed nthms)
    25.5      val ({elapsed, ...}, thm) =
    25.6        SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
    25.7 -      handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
    25.8 +        handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
    25.9      val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats
   25.10    in (Inttab.update (id, (fixes, thm)) proofs, stats') end
   25.11  
    26.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Mar 05 13:57:25 2016 +0100
    26.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Mar 05 17:01:45 2016 +0100
    26.3 @@ -207,12 +207,12 @@
    26.4        in (outcome_code, message) end
    26.5    in
    26.6      if mode = Auto_Try then
    26.7 -      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
    26.8 +      let val (outcome_code, message) = Timeout.apply timeout go () in
    26.9          (outcome_code, if outcome_code = someN then [message ()] else [])
   26.10        end
   26.11      else
   26.12        let
   26.13 -        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
   26.14 +        val (outcome_code, message) = Timeout.apply hard_timeout go ()
   26.15          val outcome =
   26.16            if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
   26.17          val _ =
   26.18 @@ -305,7 +305,7 @@
   26.19            end
   26.20        in
   26.21          launch_provers ()
   26.22 -        handle TimeLimit.TimeOut =>
   26.23 +        handle Timeout.TIMEOUT _ =>
   26.24            (print "Sledgehammer ran out of time."; (unknownN, []))
   26.25        end
   26.26        |> `(fn (outcome_code, _) => outcome_code = someN))
    27.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 05 13:57:25 2016 +0100
    27.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 05 17:01:45 2016 +0100
    27.3 @@ -418,7 +418,7 @@
    27.4      let val thy = Proof_Context.theory_of ctxt in
    27.5        stmt_xs
    27.6        |> filter (fn (_, T) => type_match thy (T, ind_T))
    27.7 -      |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
    27.8 +      |> map_filter (try (Timeout.apply instantiate_induct_timeout
    27.9          (instantiate_induct_rule ctxt stmt p_name ax)))
   27.10      end
   27.11    | NONE => [ax])
    28.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Mar 05 13:57:25 2016 +0100
    28.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Mar 05 17:01:45 2016 +0100
    28.3 @@ -97,8 +97,8 @@
    28.4  
    28.5  fun take_time timeout tac arg =
    28.6    let val timing = Timing.start () in
    28.7 -    (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
    28.8 -    handle TimeLimit.TimeOut => Play_Timed_Out timeout
    28.9 +    (Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing)))
   28.10 +    handle Timeout.TIMEOUT _ => Play_Timed_Out timeout
   28.11    end
   28.12  
   28.13  fun resolve_fact_names ctxt names =
    29.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 05 13:57:25 2016 +0100
    29.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 05 17:01:45 2016 +0100
    29.3 @@ -296,7 +296,7 @@
    29.4                |> File.write_list prob_path
    29.5  
    29.6              val ((output, run_time), (atp_proof, outcome)) =
    29.7 -              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
    29.8 +              Timeout.apply generous_slice_timeout Isabelle_System.bash_output command
    29.9                |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
   29.10                |> fst |> split_time
   29.11                |> (fn accum as (output, _) =>
   29.12 @@ -305,7 +305,7 @@
   29.13                   |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
   29.14                     atp_problem
   29.15                   handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
   29.16 -              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
   29.17 +              handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
   29.18  
   29.19              val outcome =
   29.20                (case outcome of
    30.1 --- a/src/HOL/Tools/try0.ML	Sat Mar 05 13:57:25 2016 +0100
    30.2 +++ b/src/HOL/Tools/try0.ML	Sat Mar 05 17:01:45 2016 +0100
    30.3 @@ -27,7 +27,7 @@
    30.4  fun can_apply timeout_opt pre post tac st =
    30.5    let val {goal, ...} = Proof.goal st in
    30.6      (case (case timeout_opt of
    30.7 -            SOME timeout => TimeLimit.timeLimit timeout
    30.8 +            SOME timeout => Timeout.apply timeout
    30.9            | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
   30.10        SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal
   30.11      | NONE => false)
    31.1 --- a/src/Pure/Concurrent/time_limit.ML	Sat Mar 05 13:57:25 2016 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,38 +0,0 @@
    31.4 -(*  Title:      Pure/Concurrent/time_limit.ML
    31.5 -    Author:     Makarius
    31.6 -
    31.7 -Execution with time limit (relative timeout).
    31.8 -*)
    31.9 -
   31.10 -signature TIME_LIMIT =
   31.11 -sig
   31.12 -  exception TimeOut
   31.13 -  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
   31.14 -end;
   31.15 -
   31.16 -structure TimeLimit: TIME_LIMIT =
   31.17 -struct
   31.18 -
   31.19 -exception TimeOut;
   31.20 -
   31.21 -fun timeLimit timeout f x =
   31.22 -  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
   31.23 -    let
   31.24 -      val self = Thread.self ();
   31.25 -
   31.26 -      val request =
   31.27 -        Event_Timer.request (Time.+ (Time.now (), timeout))
   31.28 -          (fn () => Standard_Thread.interrupt_unsynchronized self);
   31.29 -
   31.30 -      val result =
   31.31 -        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
   31.32 -
   31.33 -      val was_timeout = not (Event_Timer.cancel request);
   31.34 -      val test = Exn.capture Multithreading.interrupted ();
   31.35 -    in
   31.36 -      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
   31.37 -      then raise TimeOut
   31.38 -      else (Exn.release test; Exn.release result)
   31.39 -    end);
   31.40 -
   31.41 -end;
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/Pure/Concurrent/timeout.ML	Sat Mar 05 17:01:45 2016 +0100
    32.3 @@ -0,0 +1,42 @@
    32.4 +(*  Title:      Pure/Concurrent/timeout.ML
    32.5 +    Author:     Makarius
    32.6 +
    32.7 +Execution with (relative) timeout.
    32.8 +*)
    32.9 +
   32.10 +signature TIMEOUT =
   32.11 +sig
   32.12 +  exception TIMEOUT of Time.time
   32.13 +  val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
   32.14 +  val print: Time.time -> string
   32.15 +end;
   32.16 +
   32.17 +structure Timeout: TIMEOUT =
   32.18 +struct
   32.19 +
   32.20 +exception TIMEOUT of Time.time;
   32.21 +
   32.22 +fun apply timeout f x =
   32.23 +  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
   32.24 +    let
   32.25 +      val self = Thread.self ();
   32.26 +      val start = Time.now ();
   32.27 +
   32.28 +      val request =
   32.29 +        Event_Timer.request (Time.+ (start, timeout))
   32.30 +          (fn () => Standard_Thread.interrupt_unsynchronized self);
   32.31 +      val result =
   32.32 +        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
   32.33 +
   32.34 +      val stop = Time.now ();
   32.35 +      val was_timeout = not (Event_Timer.cancel request);
   32.36 +      val test = Exn.capture Multithreading.interrupted ();
   32.37 +    in
   32.38 +      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
   32.39 +      then raise TIMEOUT (Time.- (stop, start))
   32.40 +      else (Exn.release test; Exn.release result)
   32.41 +    end);
   32.42 +
   32.43 +fun print t = "Timeout after " ^ Time.toString t ^ "s";
   32.44 +
   32.45 +end;
    33.1 --- a/src/Pure/Isar/runtime.ML	Sat Mar 05 13:57:25 2016 +0100
    33.2 +++ b/src/Pure/Isar/runtime.ML	Sat Mar 05 17:01:45 2016 +0100
    33.3 @@ -112,7 +112,7 @@
    33.4          let
    33.5            val msg =
    33.6              (case exn of
    33.7 -              TimeLimit.TimeOut => "Timeout"
    33.8 +              Timeout.TIMEOUT t => Timeout.print t
    33.9              | TOPLEVEL_ERROR => "Error"
   33.10              | ERROR "" => "Error"
   33.11              | ERROR msg => msg
    34.1 --- a/src/Pure/ROOT	Sat Mar 05 13:57:25 2016 +0100
    34.2 +++ b/src/Pure/ROOT	Sat Mar 05 17:01:45 2016 +0100
    34.3 @@ -19,7 +19,7 @@
    34.4      "Concurrent/standard_thread.ML"
    34.5      "Concurrent/synchronized.ML"
    34.6      "Concurrent/task_queue.ML"
    34.7 -    "Concurrent/time_limit.ML"
    34.8 +    "Concurrent/timeout.ML"
    34.9      "Concurrent/unsynchronized.ML"
   34.10      "General/alist.ML"
   34.11      "General/antiquote.ML"
    35.1 --- a/src/Pure/ROOT.ML	Sat Mar 05 13:57:25 2016 +0100
    35.2 +++ b/src/Pure/ROOT.ML	Sat Mar 05 17:01:45 2016 +0100
    35.3 @@ -203,7 +203,7 @@
    35.4  use "Concurrent/task_queue.ML";
    35.5  use "Concurrent/future.ML";
    35.6  use "Concurrent/event_timer.ML";
    35.7 -use "Concurrent/time_limit.ML";
    35.8 +use "Concurrent/timeout.ML";
    35.9  use "Concurrent/lazy.ML";
   35.10  use "Concurrent/par_list.ML";
   35.11  
    36.1 --- a/src/Tools/quickcheck.ML	Sat Mar 05 13:57:25 2016 +0100
    36.2 +++ b/src/Tools/quickcheck.ML	Sat Mar 05 17:01:45 2016 +0100
    36.3 @@ -282,9 +282,9 @@
    36.4  
    36.5  fun limit timeout (limit_time, is_interactive) f exc () =
    36.6    if limit_time then
    36.7 -    TimeLimit.timeLimit timeout f ()
    36.8 -      handle TimeLimit.TimeOut =>
    36.9 -        if is_interactive then exc () else raise TimeLimit.TimeOut
   36.10 +    Timeout.apply timeout f ()
   36.11 +      handle timeout_exn as Timeout.TIMEOUT _ =>
   36.12 +        if is_interactive then exc () else Exn.reraise timeout_exn
   36.13    else f ();
   36.14  
   36.15  fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
    37.1 --- a/src/Tools/try.ML	Sat Mar 05 13:57:25 2016 +0100
    37.2 +++ b/src/Tools/try.ML	Sat Mar 05 17:01:45 2016 +0100
    37.3 @@ -110,7 +110,7 @@
    37.4                val auto_time_limit = Options.default_real @{system_option auto_time_limit}
    37.5              in
    37.6                if auto_time_limit > 0.0 then
    37.7 -                (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
    37.8 +                (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of
    37.9                    (true, (_, outcome)) => List.app Output.information outcome
   37.10                  | _ => ())
   37.11                else ()