src/HOL/Tools/ATP/atp_problem_generate.ML

         |> (fn T_args => IConst (name, T, T_args))
       | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
       | filt _ tm = tm
   in filt 0 end
 
-fun iformula_from_prop ctxt type_enc eq_as_iff =
+fun iformula_from_prop ctxt type_enc iff_for_eq =
   let
     val thy = Proof_Context.theory_of ctxt
     fun do_term bs t atomic_Ts =
       iterm_from_term thy type_enc bs (Envir.eta_contract t)
       |>> (introduce_proxies_in_iterm type_enc

       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
       | @{const HOL.implies} $ t1 $ t2 =>
         do_conn bs AImplies (Option.map not pos) t1 pos t2
       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
-        if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
+        if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
       | _ => do_term bs t
   in do_formula [] end
 
 fun presimplify_term thy t =
   if exists_Const (member (op =) Meson.presimplified_consts o fst) t then

       |> presimplify_term thy
       |> HOLogic.dest_Trueprop
   end
   handle TERM _ => @{const True}
 
-fun make_formula ctxt type_enc eq_as_iff name stature kind t =
-  let
+(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
+   for obscure technical reasons. *)
+fun should_use_iff_for_eq CNF _ = false
+  | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
+  | should_use_iff_for_eq _ _ = true
+
+fun make_formula ctxt format type_enc iff_for_eq name stature kind t =
+  let
+    val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
     val (iformula, atomic_Ts) =
-      iformula_from_prop ctxt type_enc eq_as_iff (SOME (kind <> Conjecture)) t
+      iformula_from_prop ctxt type_enc iff_for_eq (SOME (kind <> Conjecture)) t
                          []
       |>> close_iformula_universally
   in
     {name = name, stature = stature, kind = kind, iformula = iformula,
      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 is_format_eq_as_iff format) name
-                         stature Axiom of
+fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) =
+  case t |> make_formula ctxt format type_enc iff_for_eq name stature Axiom of
     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
     if s = tptp_true then NONE else SOME formula
   | formula => SOME formula
 
 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t

 *)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (kind, t)) =>
           t |> kind = Conjecture ? s_not
-            |> make_formula ctxt type_enc (is_format_eq_as_iff format) name
-                            stature kind)
+            |> make_formula ctxt format type_enc true name stature kind)
 
 (** Finite and infinite type inference **)
 
 fun tvar_footprint thy s ary =
   (case unprefix_and_unascii const_prefix s of