# HG changeset patch
# User wenzelm
# Date 1457193705 -3600
# Node ID a564458f94db9654fec0290706d106f4f096f8ed
# Parent  b8efcc9edd7b5984d28e71b9909862a30440e3fa
tuned signature -- clarified modules;

diff -r b8efcc9edd7b -r a564458f94db NEWS
--- a/NEWS	Sat Mar 05 13:57:25 2016 +0100
+++ b/NEWS	Sat Mar 05 17:01:45 2016 +0100
@@ -197,6 +197,10 @@
 balanced blocks of Local_Theory.open_target versus
 Local_Theory.close_target instead. Rare INCOMPATIBILITY.
 
+* Structure TimeLimit (originally from the SML/NJ library) has been
+replaced by structure Timeout, with slightly different signature.
+INCOMPATIBILITY.
+
 
 *** System ***
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Library/Old_SMT/old_smt_config.ML
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -177,8 +177,8 @@
 (* tools *)
 
 fun with_timeout ctxt f x =
-  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
-  handle TimeLimit.TimeOut => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
+  Timeout.apply (seconds (Config.get ctxt timeout)) f x
+    handle Timeout.TIMEOUT _ => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
 
 
 (* certificates *)
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Library/refute.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -1031,7 +1031,7 @@
           let
             val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
             val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
-                    orelse raise TimeLimit.TimeOut
+                    orelse raise Timeout.TIMEOUT (Time.fromMilliseconds msecs_spent)
             val init_model = (universe, [])
             val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
               bounds = [], wellformed = True}
@@ -1115,9 +1115,9 @@
       ^ (if negate then "refutes" else "satisfies") ^ ": "
       ^ Syntax.string_of_term ctxt t);
     if maxtime > 0 then (
-      TimeLimit.timeLimit (Time.fromSeconds maxtime)
+      Timeout.apply (Time.fromSeconds maxtime)
         wrapper ()
-      handle TimeLimit.TimeOut =>
+      handle Timeout.TIMEOUT _ =>
         (writeln ("Search terminated, time limit (" ^
             string_of_int maxtime
             ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -156,7 +156,7 @@
     val {context = ctxt, facts, goal} = Proof.goal st
     val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
   in
-    (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
+    (case try (Timeout.apply time (Seq.pull o full_tac)) goal of
       SOME (SOME _) => true
     | _ => false)
   end
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -14,7 +14,7 @@
   if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
   then log (arith_tag id ^ "succeeded")
   else ()
-  handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
+  handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout")
 
 fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -27,7 +27,7 @@
     |> add_info
     |> log
   end
-  handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+  handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout")
        | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
 
 fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -15,11 +15,11 @@
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
   in
-    (case TimeLimit.timeLimit timeout quickcheck pre of
+    (case Timeout.apply timeout quickcheck pre of
       NONE => log (qc_tag id ^ "no counterexample")
     | SOME _ => log (qc_tag id ^ "counterexample found"))
   end
-  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
+  handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout")
        | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
 
 fun invoke args =
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle_refute.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -14,7 +14,7 @@
     val thm = #goal (Proof.raw_goal st)
 
     val refute = Refute.refute_goal thy args thm
-    val _ = TimeLimit.timeLimit timeout refute subgoal
+    val _ = Timeout.apply timeout refute subgoal
   in
     val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
     val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -404,7 +404,7 @@
     val time_limit =
       (case hard_timeout of
         NONE => I
-      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
+      | SOME secs => Timeout.apply (Time.fromSeconds secs))
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], used_from = [],
         preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime,
@@ -434,7 +434,7 @@
           {comment = "", state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
       in prover params problem end)) ()
-      handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
+      handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     val time_prover = run_time |> Time.toMilliseconds
     val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts
@@ -590,7 +590,7 @@
           "succeeded (" ^ string_of_int t ^ ")")
     fun timed_method named_thms =
       (with_time (Mirabelle.cpu_time apply_method named_thms), true)
-      handle TimeLimit.TimeOut => (change_data id inc_proof_method_timeout; ("timeout", false))
+      handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false))
            | ERROR msg => ("error: " ^ msg, false)
 
     val _ = log separator
@@ -628,7 +628,7 @@
             if AList.lookup (op =) args check_trivialK |> the_default trivial_default
                             |> Markup.parse_bool then
               Try0.try0 (SOME try_timeout) ([], [], [], []) pre
-              handle TimeLimit.TimeOut => false
+              handle Timeout.TIMEOUT _ => false
             else false
           fun apply_method () =
             (Mirabelle.catch_result (proof_method_tag meth) false
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mirabelle/Tools/mirabelle_try0.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -13,10 +13,10 @@
 fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
 
 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
-  if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
+  if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
   then log (try0_tag id ^ "succeeded")
   else ()
-  handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")
+  handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout")
 
 fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done)
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -110,7 +110,7 @@
 (** quickcheck **)
 
 fun invoke_quickcheck change_options thy t =
-  TimeLimit.timeLimit (seconds 30.0)
+  Timeout.apply (seconds 30.0)
       (fn _ =>
           let
             val ctxt' = change_options (Proof_Context.init_global thy)
@@ -123,7 +123,7 @@
               NONE => (NoCex, Quickcheck.timings_of result)
             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
           end) ()
-  handle TimeLimit.TimeOut =>
+  handle Timeout.TIMEOUT _ =>
          (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
 
 fun quickcheck_mtd change_options quickcheck_generator =
@@ -314,7 +314,7 @@
   let
     val ctxt = Proof_Context.init_global thy
   in
-    can (TimeLimit.timeLimit (seconds 30.0)
+    can (Timeout.apply (seconds 30.0)
       (Quickcheck.test_terms
         ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
           Config.put Quickcheck.finite_types true #>
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Mar 05 17:01:45 2016 +0100
@@ -162,14 +162,14 @@
       Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
     val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
     val (mono_free_Ts, nonmono_free_Ts) =
-      TimeLimit.timeLimit mono_timeout
+      Timeout.apply mono_timeout
           (List.partition is_type_actually_monotonic) free_Ts
   in
     if not (null mono_free_Ts) then "MONO"
     else if not (null nonmono_free_Ts) then "NONMONO"
     else "NIX"
   end
-  handle TimeLimit.TimeOut => "TIMEOUT"
+  handle Timeout.TIMEOUT _ => "TIMEOUT"
        | NOT_SUPPORTED _ => "UNSUP"
        | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
 
@@ -182,11 +182,11 @@
         val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
         val neg_t = Logic.mk_implies (t, @{prop False})
         val (nondef_ts, def_ts, _, _, _, _) =
-          TimeLimit.timeLimit preproc_timeout (preprocess_formulas hol_ctxt [])
+          Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
                               neg_t
         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
       in File.append path (res ^ "\n"); writeln res end
-      handle TimeLimit.TimeOut => ()
+      handle Timeout.TIMEOUT _ => ()
   in thy |> theorems_of |> List.app check_theorem end
 *}
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Sat Mar 05 17:01:45 2016 +0100
@@ -35,7 +35,7 @@
 ML {*
   (*default timeout is 1 min*)
   fun interpret timeout file thy =
-    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
+    Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
      (TPTP_Interpret.interpret_file
        false
        [Path.explode "$TPTP"]
diff -r b8efcc9edd7b -r a564458f94db src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -1060,7 +1060,7 @@
           tactic takes too long*)
         val try_make_step =
           (*FIXME const timeout*)
-          (* TimeLimit.timeLimit (Time.fromSeconds 5) *)
+          (* Timeout.apply (Time.fromSeconds 5) *)
           (fn ctxt' =>
              let
                fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
diff -r b8efcc9edd7b -r a564458f94db src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sat Mar 05 17:01:45 2016 +0100
@@ -634,7 +634,7 @@
     let
       val timer = Timer.startRealTimer ()
     in
-      TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
+      Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
        (test_partial_reconstruction thy
         #> light_output ? erase_inference_fmlas
         #> @{make_string} (* FIXME *)
@@ -662,7 +662,7 @@
         |> Path.implode
         |> TPTP_Problem_Name.Nonstandard
     in
-      TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
+      Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
        (fn prob_name =>
         (can
           (TPTP_Reconstruct.reconstruct ctxt (fn prob_name =>
diff -r b8efcc9edd7b -r a564458f94db src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -137,10 +137,8 @@
   let
     val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
     val result =
-      TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
-      handle
-        TimeLimit.TimeOut => NONE
-      | ERROR _ => NONE
+      Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
+        handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
   in
     (case result of
       NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
diff -r b8efcc9edd7b -r a564458f94db src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -63,11 +63,11 @@
       arguments ctxt false "" atp_timeout (File.shell_path prob_file)
                 (ord, K [], K [])
     val outcome =
-      TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command
+      Timeout.apply atp_timeout Isabelle_System.bash_output command
       |> fst
       |> extract_tstplike_proof_and_outcome false proof_delims known_failures
       |> snd
-      handle TimeLimit.TimeOut => SOME TimedOut
+      handle Timeout.TIMEOUT _ => SOME TimedOut
     val _ =
       tracing ("Ran ATP: " ^
                (case outcome of
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -633,7 +633,7 @@
 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
 
 fun get_remote_systems () =
-  TimeLimit.timeLimit (seconds 10.0) (fn () =>
+  Timeout.apply (seconds 10.0) (fn () =>
     (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
       (output, 0) => split_lines output
     | (output, _) =>
@@ -641,7 +641,7 @@
          (case extract_known_atp_failure known_perl_failures output of
            SOME failure => string_of_atp_failure failure
          | NONE => trim_line output ^ "."); []))) ()
-  handle TimeLimit.TimeOut => []
+  handle Timeout.TIMEOUT _ => []
 
 fun find_remote_system name [] systems =
     find_first (String.isPrefix (name ^ "---")) systems
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -211,6 +211,7 @@
 fun pick_them_nits_in_term deadline state (params : params) mode i n step
                            subst def_assm_ts nondef_assm_ts orig_t =
   let
+    val time_start = Time.now ()
     val timer = Timer.startRealTimer ()
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -248,10 +249,11 @@
     val print_v = pprint_v o K o plazy
 
     fun check_deadline () =
-      if Time.compare (Time.now (), deadline) <> LESS then
-        raise TimeLimit.TimeOut
-      else
-        ()
+      let val t = Time.now () in
+        if Time.compare (t, deadline) <> LESS
+        then raise Timeout.TIMEOUT (Time.- (t, time_start))
+        else ()
+      end
 
     val (def_assm_ts, nondef_assm_ts) =
       if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
@@ -376,9 +378,9 @@
        (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
       is_number_type ctxt T orelse is_bit_type T
     fun is_type_actually_monotonic T =
-      TimeLimit.timeLimit tac_timeout (formulas_monotonic hol_ctxt binarize T)
+      Timeout.apply tac_timeout (formulas_monotonic hol_ctxt binarize T)
                           (nondef_ts, def_ts)
-      handle TimeLimit.TimeOut => false
+        handle Timeout.TIMEOUT _ => false
     fun is_type_kind_of_monotonic T =
       case triple_lookup (type_match thy) monos T of
         SOME (SOME false) => false
@@ -806,7 +808,7 @@
                 end
             end
           | KK.TimedOut unsat_js =>
-            (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
+            (update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime)
           | KK.Error (s, unsat_js) =>
             (update_checked_problems problems unsat_js;
              print_v (K ("Kodkod error: " ^ s ^ "."));
@@ -958,7 +960,7 @@
     val outcome_code =
       run_batches 0 (length batches) batches
                   (false, max_potential, max_genuine, 0)
-      handle TimeLimit.TimeOut =>
+      handle Timeout.TIMEOUT _ =>
              (print_nt (fn () => excipit "ran out of time after checking");
               if !met_potential > 0 then potentialN else unknownN)
     val _ = print_v (fn () =>
@@ -986,7 +988,7 @@
         val unknown_outcome = (unknownN, [])
         val deadline = Time.+ (Time.now (), timeout)
         val outcome as (outcome_code, _) =
-          TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
+          Timeout.apply (Time.+ (timeout, timeout_bonus))
               (pick_them_nits_in_term deadline state params mode i n step subst
                                       def_assm_ts nondef_assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
@@ -999,7 +1001,7 @@
                  (print_t "% SZS status GaveUp";
                   print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
                   unknown_outcome)
-               | TimeLimit.TimeOut =>
+               | Timeout.TIMEOUT _ =>
                  (print_t "% SZS status TimedOut";
                   print_nt "Nitpick ran out of time."; unknown_outcome)
       in
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -577,18 +577,18 @@
           |> List.partition (member (op =) ["dptsat", "cdclite"] o fst)
         val res =
           if null nonml_solvers then
-            TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop
+            Timeout.apply tac_timeout (snd (hd ml_solvers)) prop
           else
-            TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop
-            handle TimeLimit.TimeOut =>
-                   TimeLimit.timeLimit tac_timeout
+            Timeout.apply ml_solver_timeout (snd (hd ml_solvers)) prop
+            handle Timeout.TIMEOUT _ =>
+                   Timeout.apply tac_timeout
                                        (SAT_Solver.invoke_solver "auto") prop
       in
         case res of
           SAT_Solver.SATISFIABLE assigns => do_assigns assigns
         | _ => (trace_msg (K "*** Unsolvable"); NONE)
       end
-      handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE)
+      handle Timeout.TIMEOUT _ => (trace_msg (K "*** Timed out"); NONE)
   end
 
 type mcontext =
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -273,7 +273,7 @@
 val eta_expand = ATP_Util.eta_expand
 
 fun DETERM_TIMEOUT delay tac st =
-  Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ()))
+  Seq.of_list (the_list (Timeout.apply delay (fn () => SINGLE tac st) ()))
 
 val indent_size = 2
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -882,7 +882,7 @@
     val args' = map (rename_vars_term renaming) args
     val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     val _ = tracing ("Generated prolog program:\n" ^ prog)
-    val solution = TimeLimit.timeLimit timeout (fn prog =>
+    val solution = Timeout.apply timeout (fn prog =>
       Isabelle_System.with_tmp_file "prolog_file" "" (fn prolog_file =>
         (File.write prolog_file prog; invoke system prolog_file))) prog
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -1890,7 +1890,7 @@
           let
             val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
           in
-            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
+            rpair NONE (Timeout.apply time_limit (fn () => fst (Limited_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict
                 (get_dseq_random_result, put_dseq_random_result,
                   "Predicate_Compile_Core.put_dseq_random_result")
@@ -1902,7 +1902,7 @@
               depth true)) ())
           end
       | DSeq =>
-          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
+          rpair NONE (Timeout.apply time_limit (fn () => fst (Limited_Sequence.yieldn k
             (Code_Runtime.dynamic_value_strict
               (get_dseq_result, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
               ctxt NONE Limited_Sequence.map t' [])
@@ -1911,7 +1911,7 @@
           let
             val depth = Code_Numeral.natural_of_integer (the_single arguments)
           in
-            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
+            rpair NONE (Timeout.apply time_limit (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict
                 (get_new_dseq_result, put_new_dseq_result,
                   "Predicate_Compile_Core.put_new_dseq_result")
@@ -1925,7 +1925,7 @@
           in
             if stats then
               apsnd (SOME o accumulate o map Code_Numeral.integer_of_natural)
-              (split_list (TimeLimit.timeLimit time_limit
+              (split_list (Timeout.apply time_limit
               (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (get_lseq_random_stats_result, put_lseq_random_stats_result,
@@ -1936,7 +1936,7 @@
                     |> Lazy_Sequence.map (apfst proc))
                     t' [] nrandom size seed depth))) ()))
             else rpair NONE
-              (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
+              (Timeout.apply time_limit (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (get_lseq_random_result, put_lseq_random_result,
                     "Predicate_Compile_Core.put_lseq_random_result")
@@ -1947,11 +1947,11 @@
                       t' [] nrandom size seed depth))) ())
           end
       | _ =>
-          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
+          rpair NONE (Timeout.apply time_limit (fn () => fst (Predicate.yieldn k
             (Code_Runtime.dynamic_value_strict
               (get_pred_result, put_pred_result, "Predicate_Compile_Core.put_pred_result")
               ctxt NONE Predicate.map t' []))) ()))
-     handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
+     handle Timeout.TIMEOUT _ => error "Reached timeout during execution of values"
   in ((T, ts), statistics) end;
 
 fun values param_user_modes ((raw_expected, stats), comp_options) k t_compr ctxt =
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -196,8 +196,8 @@
 (* tools *)
 
 fun with_time_limit ctxt timeout_config f x =
-  TimeLimit.timeLimit (seconds (Config.get ctxt timeout_config)) f x
-  handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+  Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
+    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
 
 fun with_timeout ctxt = with_time_limit ctxt timeout
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/SMT/z3_replay.ML
--- a/src/HOL/Tools/SMT/z3_replay.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -72,7 +72,7 @@
     val replay = Timing.timing (replay_thm ctxt assumed nthms)
     val ({elapsed, ...}, thm) =
       SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
-      handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+        handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
     val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats
   in (Inttab.update (id, (fixes, thm)) proofs, stats') end
 
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -207,12 +207,12 @@
       in (outcome_code, message) end
   in
     if mode = Auto_Try then
-      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+      let val (outcome_code, message) = Timeout.apply timeout go () in
         (outcome_code, if outcome_code = someN then [message ()] else [])
       end
     else
       let
-        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
+        val (outcome_code, message) = Timeout.apply hard_timeout go ()
         val outcome =
           if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
         val _ =
@@ -305,7 +305,7 @@
           end
       in
         launch_provers ()
-        handle TimeLimit.TimeOut =>
+        handle Timeout.TIMEOUT _ =>
           (print "Sledgehammer ran out of time."; (unknownN, []))
       end
       |> `(fn (outcome_code, _) => outcome_code = someN))
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -418,7 +418,7 @@
     let val thy = Proof_Context.theory_of ctxt in
       stmt_xs
       |> filter (fn (_, T) => type_match thy (T, ind_T))
-      |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
+      |> map_filter (try (Timeout.apply instantiate_induct_timeout
         (instantiate_induct_rule ctxt stmt p_name ax)))
     end
   | NONE => [ax])
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -97,8 +97,8 @@
 
 fun take_time timeout tac arg =
   let val timing = Timing.start () in
-    (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
-    handle TimeLimit.TimeOut => Play_Timed_Out timeout
+    (Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing)))
+    handle Timeout.TIMEOUT _ => Play_Timed_Out timeout
   end
 
 fun resolve_fact_names ctxt names =
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -296,7 +296,7 @@
               |> File.write_list prob_path
 
             val ((output, run_time), (atp_proof, outcome)) =
-              TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
+              Timeout.apply 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, _) =>
@@ -305,7 +305,7 @@
                  |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
                    atp_problem
                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
-              handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
+              handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
 
             val outcome =
               (case outcome of
diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/try0.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -27,7 +27,7 @@
 fun can_apply timeout_opt pre post tac st =
   let val {goal, ...} = Proof.goal st in
     (case (case timeout_opt of
-            SOME timeout => TimeLimit.timeLimit timeout
+            SOME timeout => Timeout.apply timeout
           | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
       SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal
     | NONE => false)
diff -r b8efcc9edd7b -r a564458f94db src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Sat Mar 05 13:57:25 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(*  Title:      Pure/Concurrent/time_limit.ML
-    Author:     Makarius
-
-Execution with time limit (relative timeout).
-*)
-
-signature TIME_LIMIT =
-sig
-  exception TimeOut
-  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end;
-
-structure TimeLimit: TIME_LIMIT =
-struct
-
-exception TimeOut;
-
-fun timeLimit timeout f x =
-  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
-    let
-      val self = Thread.self ();
-
-      val request =
-        Event_Timer.request (Time.+ (Time.now (), timeout))
-          (fn () => Standard_Thread.interrupt_unsynchronized self);
-
-      val result =
-        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
-
-      val was_timeout = not (Event_Timer.cancel request);
-      val test = Exn.capture Multithreading.interrupted ();
-    in
-      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
-      then raise TimeOut
-      else (Exn.release test; Exn.release result)
-    end);
-
-end;
diff -r b8efcc9edd7b -r a564458f94db src/Pure/Concurrent/timeout.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/timeout.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -0,0 +1,42 @@
+(*  Title:      Pure/Concurrent/timeout.ML
+    Author:     Makarius
+
+Execution with (relative) timeout.
+*)
+
+signature TIMEOUT =
+sig
+  exception TIMEOUT of Time.time
+  val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
+  val print: Time.time -> string
+end;
+
+structure Timeout: TIMEOUT =
+struct
+
+exception TIMEOUT of Time.time;
+
+fun apply timeout f x =
+  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+    let
+      val self = Thread.self ();
+      val start = Time.now ();
+
+      val request =
+        Event_Timer.request (Time.+ (start, timeout))
+          (fn () => Standard_Thread.interrupt_unsynchronized self);
+      val result =
+        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+
+      val stop = Time.now ();
+      val was_timeout = not (Event_Timer.cancel request);
+      val test = Exn.capture Multithreading.interrupted ();
+    in
+      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+      then raise TIMEOUT (Time.- (stop, start))
+      else (Exn.release test; Exn.release result)
+    end);
+
+fun print t = "Timeout after " ^ Time.toString t ^ "s";
+
+end;
diff -r b8efcc9edd7b -r a564458f94db src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Pure/Isar/runtime.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -112,7 +112,7 @@
         let
           val msg =
             (case exn of
-              TimeLimit.TimeOut => "Timeout"
+              Timeout.TIMEOUT t => Timeout.print t
             | TOPLEVEL_ERROR => "Error"
             | ERROR "" => "Error"
             | ERROR msg => msg
diff -r b8efcc9edd7b -r a564458f94db src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Pure/ROOT	Sat Mar 05 17:01:45 2016 +0100
@@ -19,7 +19,7 @@
     "Concurrent/standard_thread.ML"
     "Concurrent/synchronized.ML"
     "Concurrent/task_queue.ML"
-    "Concurrent/time_limit.ML"
+    "Concurrent/timeout.ML"
     "Concurrent/unsynchronized.ML"
     "General/alist.ML"
     "General/antiquote.ML"
diff -r b8efcc9edd7b -r a564458f94db src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Pure/ROOT.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -203,7 +203,7 @@
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
 use "Concurrent/event_timer.ML";
-use "Concurrent/time_limit.ML";
+use "Concurrent/timeout.ML";
 use "Concurrent/lazy.ML";
 use "Concurrent/par_list.ML";
 
diff -r b8efcc9edd7b -r a564458f94db src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Tools/quickcheck.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -282,9 +282,9 @@
 
 fun limit timeout (limit_time, is_interactive) f exc () =
   if limit_time then
-    TimeLimit.timeLimit timeout f ()
-      handle TimeLimit.TimeOut =>
-        if is_interactive then exc () else raise TimeLimit.TimeOut
+    Timeout.apply timeout f ()
+      handle timeout_exn as Timeout.TIMEOUT _ =>
+        if is_interactive then exc () else Exn.reraise timeout_exn
   else f ();
 
 fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
diff -r b8efcc9edd7b -r a564458f94db src/Tools/try.ML
--- a/src/Tools/try.ML	Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Tools/try.ML	Sat Mar 05 17:01:45 2016 +0100
@@ -110,7 +110,7 @@
               val auto_time_limit = Options.default_real @{system_option auto_time_limit}
             in
               if auto_time_limit > 0.0 then
-                (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
+                (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of
                   (true, (_, outcome)) => List.app Output.information outcome
                 | _ => ())
               else ()