--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 06 13:37:49 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 06 13:46:26 2011 +0100
@@ -91,9 +91,7 @@
fun can_min_fast_enough msecs =
0.001 * Real.fromInt ((num_facts + 2) * msecs)
<= Config.get ctxt auto_minimize_max_time
- val prover_fast_enough =
- run_time_in_msecs |> Option.map can_min_fast_enough
- |> the_default false
+ val prover_fast_enough = can_min_fast_enough run_time_in_msecs
in
if isar_proof then
((prover_fast_enough, name), preplay)