src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 43982 05ff40b255eb
parent 43962 e1d29c3ca933
child 43998 a2aa341bc658
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jul 26 14:53:00 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jul 26 14:53:00 2011 +0200
@@ -821,7 +821,8 @@
                   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
                    ());