src/HOL/Tools/Sledgehammer/sledgehammer.ML

             plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
             |> Output.urgent_message
           else
             ()
         val {outcome, used_facts, run_time_in_msecs} =
-          TimeLimit.timeLimit iter_timeout
-              (SMT_Solver.smt_filter remote iter_timeout state facts) i
-          handle TimeLimit.TimeOut =>
-                 {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
-                  run_time_in_msecs = NONE}
+          SMT_Solver.smt_filter remote iter_timeout state facts i
         val _ =
           if verbose andalso is_some outcome then
             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
             |> Output.urgent_message
           else