--- 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)