# HG changeset patch
# User blanchet
# Date 1280438647 -7200
# Node ID 4339b1acfd4fb5253103f68dda561c2ef8a37dc3
# Parent  019a49759829856c5d400622f662865edf9b405b
make Mirabelle happy

diff -r 019a49759829 -r 4339b1acfd4f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 29 23:11:35 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 29 23:24:07 2010 +0200
@@ -306,7 +306,8 @@
       ctxt
       |> change_dir dir
       |> Config.put Sledgehammer.measure_runtime true
-    val params = Sledgehammer_Isar.default_params thy []
+    val params = Sledgehammer_Isar.default_params thy
+      [("timeout", Int.toString timeout)]
     val problem =
       {subgoal = 1, goal = (ctxt', (facts, goal)),
        relevance_override = {add = [], del = [], only = false}, axioms = NONE}
@@ -317,7 +318,7 @@
     val ({outcome, message, used_thm_names,
           atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time
-                      (prover params (K "") (Time.fromSeconds timeout))) problem
+                      (prover params (K ""))) problem
   in
     case outcome of
       NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
@@ -380,7 +381,6 @@
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     open Metis_Clauses
-    open Sledgehammer_Isar
     val thy = Proof.theory_of st
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_atp thy args
@@ -388,7 +388,7 @@
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
       |> the_default 5
-    val params = default_params thy
+    val params = Sledgehammer_Isar.default_params thy
       [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
     val minimize =
       Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)