remove spurious message
authorblanchet
Tue, 26 Jul 2011 14:53:00 +0200
changeset 4485305ff40b255eb
parent 44852 404ae49ce29f
child 44854 c51b4196b5e6
remove spurious message
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jul 26 14:53:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jul 26 14:53:00 2011 +0200
     1.3 @@ -821,7 +821,8 @@
     1.4                    facts |> map untranslated_fact |> filter_used_facts used_facts
     1.5                          |> map snd
     1.6                in
     1.7 -                (if mode = Minimize then
     1.8 +                (if mode = Minimize andalso
     1.9 +                    Time.> (preplay_timeout, Time.zeroTime) then
    1.10                     Output.urgent_message "Preplaying proof..."
    1.11                   else
    1.12                     ());