diff -r ccb1d4874f63 -r 024cf0f7fb6d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 26 00:33:47 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 26 01:05:06 2012 +0200
@@ -1257,8 +1257,15 @@
      atomic_types = atomic_Ts}
   end
 
+(* Satallax prefers "=" to "<=>" *)
+fun is_format_eq_as_iff FOF = true
+  | is_format_eq_as_iff (TFF _) = true
+  | is_format_eq_as_iff (DFG _) = true
+  | is_format_eq_as_iff _ = false
+
 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
-  case t |> make_formula ctxt type_enc (eq_as_iff andalso format <> CNF) name
+  case t |> make_formula ctxt type_enc
+                         (eq_as_iff andalso is_format_eq_as_iff format) name
                          stature Axiom of
     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
     if s = tptp_true then NONE else SOME formula
@@ -1274,7 +1281,8 @@
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (kind, t)) =>
           t |> kind = Conjecture ? s_not
-            |> make_formula ctxt type_enc (format <> CNF) name stature kind)
+            |> make_formula ctxt type_enc (is_format_eq_as_iff format) name
+                            stature kind)
 
 (** Finite and infinite type inference **)