--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 01 13:18:27 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 01 13:18:27 2011 +0200
@@ -378,8 +378,7 @@
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
- force_sos |> the_default I)
- #> Config.put Sledgehammer_Provers.measure_run_time true)
+ force_sos |> the_default I))
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),