--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:46:26 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:57:17 2011 +0100
@@ -70,7 +70,7 @@
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
- val result as {outcome, used_facts, run_time_in_msecs, ...} =
+ val result as {outcome, used_facts, run_time, ...} =
prover params (K (K "")) problem
in
print silent
@@ -80,9 +80,8 @@
| NONE =>
"Found proof" ^
(if length used_facts = length facts then ""
- else " with " ^ n_facts used_facts) ^ " (" ^
- string_from_time (Time.fromMilliseconds run_time_in_msecs) ^
- ").");
+ else " with " ^ n_facts used_facts) ^
+ " (" ^ string_from_time run_time ^ ").");
result
end