src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML

     val max_imperfect =
       Real.ceil (Math.pow (max_imperfect,
         Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp)))
     val (perfect, imperfect) = candidates
       |> sort (Real.compare o swap o apply2 snd)
-      |> take_prefix (fn (_, w) => w > 0.99999)
+      |> chop_prefix (fn (_, w) => w > 0.99999)
     val ((accepts, more_rejects), rejects) =
       chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   in
     trace_msg ctxt (fn () =>
       "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^