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 ());