diff -r 4339b1acfd4f -r 8fbf60c33794 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 29 23:24:07 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 29 23:37:10 2010 +0200
@@ -307,7 +307,7 @@
       |> change_dir dir
       |> Config.put Sledgehammer.measure_runtime true
     val params = Sledgehammer_Isar.default_params thy
-      [("timeout", Int.toString timeout)]
+      [("timeout", Int.toString timeout ^ " s")]
     val problem =
       {subgoal = 1, goal = (ctxt', (facts, goal)),
        relevance_override = {add = [], del = [], only = false}, axioms = NONE}
@@ -389,7 +389,7 @@
       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params thy
-      [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
+      [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
     val minimize =
       Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator