src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML

         fun rest memo' ctxt' = skel_to_naive_tactic_dbg prover_tac ctxt' prob_name (tl skel) memo'
         (*reconstruct the inference. also set timeout in case
           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)
                val reconstructed_inference = thm ctxt'
                fun rec_inf_tac st = HEADGOAL (resolve_tac ctxt' [thm ctxt']) st