src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

               let
                 val used_ths =
                   facts |> map untranslated_fact |> filter_used_facts used_facts
                         |> map snd
               in
-                (if mode = Minimize then
+                (if mode = Minimize andalso
+                    Time.> (preplay_timeout, Time.zeroTime) then
                    Output.urgent_message "Preplaying proof..."
                  else
                    ());
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
                                     metis_reconstructors