src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

   is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
 
 fun default_max_facts_of_prover ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     if is_atp thy name then
-      fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
+      fold (Integer.max o fst o #1) (#best_slices (get_atp thy name ()) ctxt) 0
     else if is_smt_prover ctxt name then
       SMT_Solver.default_max_relevant ctxt name
     else
       error ("No such prover: " ^ name)
   end