src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
changeset 61612 40859aa6d10c
parent 59058 a78612c67ec0
child 61666 f1b257607981
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Nov 10 17:49:54 2015 +0100
@@ -214,10 +214,11 @@
                 NONE => steps
               | SOME times0 =>
                 let
-                  val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l)
-                  val timeouts =
-                    map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
-                  val meths_outcomess = @{map 3} (preplay_isar_step ctxt) timeouts hopelesses succs'
+                  val n = length labels
+                  val total_time = Library.foldl (op Time.+) (reference_time l, times0)
+                  val timeout = adjust_merge_timeout preplay_timeout
+                    (Time.fromReal (Time.toReal total_time / Real.fromInt n))
+                  val meths_outcomess = @{map 2} (preplay_isar_step ctxt timeout) hopelesses succs'
                 in
                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
                     NONE => steps