equal
deleted
inserted
replaced
623 | choose_format formats type_sys = |
623 | choose_format formats type_sys = |
624 (case hd formats of |
624 (case hd formats of |
625 CNF_UEQ => |
625 CNF_UEQ => |
626 (CNF_UEQ, case type_sys of |
626 (CNF_UEQ, case type_sys of |
627 Preds stuff => |
627 Preds stuff => |
628 (if is_type_sys_fairly_sound type_sys then Preds else Tags) |
628 (if is_type_sys_fairly_sound type_sys then Tags else Preds) |
629 stuff |
629 stuff |
630 | _ => type_sys) |
630 | _ => type_sys) |
631 | format => (format, type_sys)) |
631 | format => (format, type_sys)) |
632 |
632 |
633 type translated_formula = |
633 type translated_formula = |