src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

               |> 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)) =
-              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, _) =>
                 (accum,
                  extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
                  |>> 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
                 NONE =>
                 (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of