equal
deleted
inserted
replaced
283 (fn (_, tag, [pat]) => (pat, tag) |
283 (fn (_, tag, [pat]) => (pat, tag) |
284 | _ => case_error "error in pattern-match translation") patts; |
284 | _ => case_error "error in pattern-match translation") patts; |
285 val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1 |
285 val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1 |
286 val finals = map row_of_pat patts2 |
286 val finals = map row_of_pat patts2 |
287 val originals = map (row_of_pat o #2) rows |
287 val originals = map (row_of_pat o #2) rows |
288 val _ = case originals \\ finals of |
288 val _ = case subtract (op =) finals originals of |
289 [] => () |
289 [] => () |
290 | is => (case config of Error => case_error | Warning => warning | Quiet => fn _ => {}) |
290 | is => (case config of Error => case_error | Warning => warning | Quiet => fn _ => {}) |
291 ("The following clauses are redundant (covered by preceding clauses):\n" ^ |
291 ("The following clauses are redundant (covered by preceding clauses):\n" ^ |
292 cat_lines (map (string_of_clause o nth clauses) is)); |
292 cat_lines (map (string_of_clause o nth clauses) is)); |
293 in |
293 in |