--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Oct 17 22:35:28 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Oct 17 23:47:27 2009 +0200
@@ -307,8 +307,8 @@
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) =
- time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
+ val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
+ time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
in
if success then (message, SH_OK (time_isa, time_atp, theorem_names))
else (message, SH_FAIL(time_isa, time_atp))