src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

               relevance_fudge relevance_override chained_ths hyp_ts concl_t
         val problem =
           {state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st,
            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
-           smt_head = NONE}
+           smt_filter = NONE}
       in prover params (K "") problem end)) ()
       handle TimeLimit.TimeOut =>
              ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
                run_time_in_msecs = NONE}, ~1)
     val time_prover = run_time_in_msecs |> the_default ~1