1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Oct 17 23:07:53 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Oct 17 23:48:09 2009 +0200
     1.3 @@ -307,8 +307,8 @@
     1.4        (case hard_timeout of
     1.5          NONE => I
     1.6        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     1.7 -    val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) =
     1.8 -      time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
     1.9 +    val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
    1.10 +        time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
    1.11    in
    1.12      if success then (message, SH_OK (time_isa, time_atp, theorem_names))
    1.13      else (message, SH_FAIL(time_isa, time_atp))