# HG changeset patch
# User wenzelm
# Date 1255816089 -7200
# Node ID 6f5efd3cfc3980500adb545ea2b374e2db23a6e1
# Parent  2ef1adff7eee102b02cccabb95a04ce62f98aeaf# Parent  fbc642835ecba753fd681e75b5141d2b7af7d93c
merged

diff -r 2ef1adff7eee -r 6f5efd3cfc39 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Oct 17 23:07:53 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Oct 17 23:48:09 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))