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