src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

     fun add_add_ths accepts =
       (facts |> filter ((member Thm.eq_thm add_ths
                          andf (not o member (Thm.eq_thm o apsnd snd) accepts))
                         o snd))
       @ accepts
+      |> take max_relevant
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
           |> iter 0 max_relevant threshold0 goal_const_tab []
           |> not (null add_ths) ? add_add_ths
           |> tap (fn res => trace_msg (fn () =>