# HG changeset patch
# User blanchet
# Date 1288881048 -3600
# Node ID f16ce22f34d01abc459abc0d3577189cbad0fbf9
# Parent  8fe3c26c49aff9d8f9f9a182681208549e4ef061
remove " s" suffix since seconds are now implicit

diff -r 8fe3c26c49af -r f16ce22f34d0 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 04 14:59:44 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 04 15:30:48 2010 +0100
@@ -349,7 +349,7 @@
                  #> Config.put Sledgehammer.measure_run_time true)
     val params as {full_types, relevance_thresholds, max_relevant, ...} =
       Sledgehammer_Isar.default_params ctxt
-          [("timeout", Int.toString timeout ^ " s")]
+          [("timeout", Int.toString timeout)]
     val default_max_relevant =
       Sledgehammer.default_max_relevant_for_prover thy prover_name
     val is_built_in_const =
@@ -446,7 +446,7 @@
       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params ctxt
-      [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
+      [("provers", prover_name), ("timeout", Int.toString timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts params 1
                                            (Sledgehammer_Util.subgoal_count st)