src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML

       |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
         hyp_ts concl_t
       |> hd |> snd
     val problem =
       {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       facts = ("", facts), found_proof = K ()}
+       factss = [("", facts)], found_proof = K ()}
+    val slice = get_default_slice ctxt name
   in
-    (case prover params problem of
+    (case prover params problem slice of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
     | _ => NONE)
     handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
   end