src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

               val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
 
               (* 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 ();
                  set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
                  map (replace_successor l' [l]) lfs';

                 let
                   val n = length labels
                   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
                   | SOME times =>
                     (* "l" successfully eliminated *)