fixed format selection logic for Waldmeister
authorblanchet
Wed, 08 Jun 2011 16:20:18 +0200
changeset 441470f2bbcfaf208
parent 44146 7a4eebdebb23
child 44148 07eb0ad9bb93
fixed format selection logic for Waldmeister
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 16:20:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 16:20:18 2011 +0200
     1.3 @@ -625,7 +625,7 @@
     1.4         CNF_UEQ =>
     1.5         (CNF_UEQ, case type_sys of
     1.6                     Preds stuff =>
     1.7 -                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
     1.8 +                   (if is_type_sys_fairly_sound type_sys then Tags else Preds)
     1.9                         stuff
    1.10                   | _ => type_sys)
    1.11       | format => (format, type_sys))