src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML

     in
       set_preplay_time l (false, time);
       mk_step_lfs_gfs min_lfs min_gfs
     end)
 
-fun minimize_dependencies_and_remove_unrefed_steps
-  isar_minimize preplay_interface proof =
+fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
+        proof =
   let
     fun cons_to xs x = x :: xs
 
     val add_lfs = fold (Ord_List.insert label_ord)
 

           else
             (refed, accu)
 
     and do_refed_step step =
       step
-      |> isar_minimize ? min_deps_of_step preplay_interface
+      |> isar_try0 ? min_deps_of_step preplay_interface
       |> do_refed_step'
 
     and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
       | do_refed_step' (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))) =
         let

             |>> add_lfs lfs
           val step = Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))
         in
           (refed, step)
         end
-
   in
     snd (do_proof proof)
   end
 
 end