# HG changeset patch
# User blanchet
# Date 1307542818 -7200
# Node ID 0f2bbcfaf208dbcb1c7c7d283a73e2583080c9a5
# Parent  7a4eebdebb230cb30186260fe09fa10dd127e79d
fixed format selection logic for Waldmeister

diff -r 7a4eebdebb23 -r 0f2bbcfaf208 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 16:20:18 2011 +0200
@@ -625,7 +625,7 @@
        CNF_UEQ =>
        (CNF_UEQ, case type_sys of
                    Preds stuff =>
-                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
+                   (if is_type_sys_fairly_sound type_sys then Tags else Preds)
                        stuff
                  | _ => type_sys)
      | format => (format, type_sys))