src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

   (*default timeout is 1 min*)
   fun reconstruct timeout light_output file thy =
     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 *)
         #> (fn s => report (Proof_Context.init_global thy) (@{make_string} file ^ " === " ^ s ^
              " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string}))))

         file
         |> Path.base
         |> 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 =>
             TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference prob_name (* oracle_based_reconstruction_tac *))) prob_name )
        |> (fn s => report ctxt (Path.print file ^ " === " ^ Bool.toString s ^