# HG changeset patch
# User wenzelm
# Date 1447505329 -3600
# Node ID f1b2576079816a1c3a7bb0002999320b2757f329
# Parent  9cb2d8acf1c013653dbd4d65b02a614dd43d454a
more standard ML, to make SML/NJ more happy;

diff -r 9cb2d8acf1c0 -r f1b257607981 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Nov 13 23:10:35 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sat Nov 14 13:48:49 2015 +0100
@@ -215,7 +215,7 @@
               | 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'