src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

                   forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of
                 NONE => steps
               | SOME times0 =>
                 let
                   val n = length labels
-                  val total_time = Library.foldl (op Time.+) (reference_time l, times0)
+                  val total_time = Library.foldl 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