src/HOL/TPTP/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 =
-      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+      {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
   in
     (case prover params (K (K (K ""))) problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
     | _ => NONE)