src/HOL/Tools/Sledgehammer/sledgehammer.ML

                 if not minimize orelse is_metis_method meth then
                   (used_facts, res)
                 else
                   let
                     val (time', used_names') =
-                      minimized_isar_step ctxt time (mk_step fact_names [meth])
+                      minimized_isar_step ctxt chained time (mk_step fact_names [meth])
                       ||> (facts_of_isar_step #> snd)
                     val used_facts' = filter (member (op =) used_names' o fst) used_facts
                   in
                     (used_facts', (meth, Played time'))
                   end