# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1447174194 -3600
# Node ID 40859aa6d10c361c41653ffe5ac39d786091a431
# Parent  a9c0572109af6a351062abb593edf2e25388e00a
generalized so that is also works for veriT proofs

diff -r a9c0572109af -r 40859aa6d10c src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- 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