--- 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'