src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML

            Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover
          val relevance_fudge =
            extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge
          val subgoal = 1
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
-         val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
+         val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover
          val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
          val facts =
            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
                Sledgehammer_Fact.no_fact_override reserved css_table chained_ths