src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML

   | keep_fastest_method_of_isar_step _ step = step
 
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs0, gfs0), meths as meth :: _))) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
 

             (case preplay_isar_step ctxt (Time.+ (time, slack)) meth
                 (mk_step (min_facts @ facts)) of
               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 (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
-        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+        val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) time [] lfs0
+        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs0
 
         val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
         set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
           [(meth, Lazy.value (Played time))];