src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML

 open Sledgehammer_Isar_Preplay
 
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
-  | minimize_isar_step_dependencies
-      {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
+  | minimize_isar_step_dependencies {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...}
       (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
     (case Lazy.force (preplay_outcome l meth) of
       Played time =>
       let
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))

               Played time => minimize_facts mk_step time min_facts facts
             | _ => minimize_facts mk_step time (f :: min_facts) facts)
 
         val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
         val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
-
-        val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
-        reset_preplay_outcomes step';
-        set_preplay_outcome l meth (Played time);
-        step'
+        set_preplay_outcomes l [(meth, Lazy.value (Played time))];
+        mk_step_lfs_gfs min_lfs min_gfs
       end
     | _ => step (* don't touch steps that time out or fail *))
 
 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
   let