remove spurious message
authorblanchet
Tue, 26 Jul 2011 14:53:00 +0200
changeset 43982 05ff40b255eb
parent 43981 404ae49ce29f
child 43983 c51b4196b5e6
remove spurious message
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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
                    ());