equal
deleted
inserted
replaced
326 (* removing duplicates, preferring nicer names, roughly O(n log n) *) |
326 (* removing duplicates, preferring nicer names, roughly O(n log n) *) |
327 |
327 |
328 local |
328 local |
329 |
329 |
330 val index_ord = option_ord (K EQUAL); |
330 val index_ord = option_ord (K EQUAL); |
331 val hidden_ord = bool_ord o apply2 Long_Name.is_hidden; |
331 val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden); |
332 val qual_ord = int_ord o apply2 Long_Name.qualification; |
332 val qual_ord = int_ord o apply2 Long_Name.qualification; |
333 val txt_ord = int_ord o apply2 size; |
333 val txt_ord = int_ord o apply2 size; |
334 |
334 |
335 fun nicer_name (x, i) (y, j) = |
335 fun nicer_name (x, i) (y, j) = |
336 (case hidden_ord (x, y) of EQUAL => |
336 (case hidden_ord (x, y) of EQUAL => |