src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

       Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
           (the_default default_max_relevant max_relevant)
           relevance_override chained_ths hyp_ts concl_t
     val problem =
       {state = st', goal = goal, subgoal = i,
-       axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
+       axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms,
+       only = true}
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     val ({outcome, message, used_thm_names,