src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = default_params thy
       [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
-    val minimize = minimize_theorems params 1 (subgoal_count st)
+    val minimize =
+      Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of
       (SOME named_thms', msg) =>
         (change_data id inc_min_succs;