src/HOL/Tools/Sledgehammer/sledgehammer.ML

           let
             val max_max_facts =
               (case max_facts of
                 SOME n => n
               | NONE =>
-                0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
+                0 |> fold (fn prover => Integer.max (fst (fst (get_default_slice ctxt prover))))
+                    provers
                   |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
             val ({elapsed, ...}, factss) = Timing.timing
               (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
               all_facts
             val () = spying spy (fn () => (state, i, "All",