--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 01 19:57:58 2016 +0100
@@ -173,7 +173,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
in
- (case preplay_isar_step ctxt timeout hopeless step'' of
+ (case preplay_isar_step ctxt [] timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
(* "l'" successfully eliminated *)
(decrement_step_count ();
@@ -218,7 +218,8 @@
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'
+ 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