# HG changeset patch
# User blanchet
# Date 1311684780 -7200
# Node ID 05ff40b255eb7a5071fbf612a055e27f3140cb5d
# Parent  404ae49ce29f05a8ffd41bb955597b10eb954bf8
remove spurious message

diff -r 404ae49ce29f -r 05ff40b255eb 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
                    ());