src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

   let
     fun default_prover_name () =
       hd (#provers (Sledgehammer_Isar.default_params ctxt []))
       handle Empty => error "No ATP available."
     fun get_prover name =
-      (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
+      (name, Sledgehammer_Run.get_minimizing_prover ctxt
+                Sledgehammer_Provers.Normal name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
     | NONE => get_prover (default_prover_name ()))
   end