# HG changeset patch
# User blanchet
# Date 1272018270 -7200
# Node ID 59a55dfa76d508276da8d1d64c22c0443dfe5c96
# Parent  e6db3ba0b61d67fed5a6d2553b8f00d4a597fd5a
compile

diff -r e6db3ba0b61d -r 59a55dfa76d5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Apr 23 12:07:12 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Apr 23 12:24:30 2010 +0200
@@ -321,7 +321,7 @@
     val ({success, message, relevant_thm_names,
           atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time
-                      (prover params (Time.fromSeconds timeout))) problem
+                      (prover params (K "") (Time.fromSeconds timeout))) problem
   in
     if success then (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     else (message, SH_FAIL (time_isa, time_atp))