src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

           val cand_ord =
             prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key
 
           fun pop_next_candidate [] = (NONE, [])
             | pop_next_candidate (cands as (cand :: cands')) =
-              fold (fn x => fn y => if cand_ord (x, y) = LESS then x else y) cands' cand
+              fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand
               |> (fn best => (SOME best, remove (op =) best cands))
 
           fun try_eliminate i l labels steps =
             let
               val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) =