--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:37:49 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:46:26 2011 +0100
@@ -80,11 +80,9 @@
| NONE =>
"Found proof" ^
(if length used_facts = length facts then ""
- else " with " ^ n_facts used_facts) ^
- (case run_time_in_msecs of
- SOME ms =>
- " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
- | NONE => "") ^ ".");
+ else " with " ^ n_facts used_facts) ^ " (" ^
+ string_from_time (Time.fromMilliseconds run_time_in_msecs) ^
+ ").");
result
end