src/HOL/Tools/ATP/atp_translate.ML
changeset 43289 0f2bbcfaf208
parent 43266 3baf384e2b99
child 43293 a80cdc4b27a3
equal deleted inserted replaced
43288:7a4eebdebb23 43289:0f2bbcfaf208
   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 =