src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML

                  is_built_in_const 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_filter = NONE}
+           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
       in prover params (K (K (K ""))) problem end)) ()
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     val time_prover = run_time |> Time.toMilliseconds
     val msg = message (preplay ()) ^ message_tail