--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 01 15:12:57 2018 +0100
@@ -199,7 +199,7 @@
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 =