author | blanchet |
Tue, 26 Jul 2011 14:53:00 +0200 | |
changeset 43982 | 05ff40b255eb |
parent 43981 | 404ae49ce29f |
child 43983 | c51b4196b5e6 |
--- 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 ());