src/HOL/Tools/ATP/atp_problem_generate.ML

   in
     {name = name, stature = stature, kind = kind, iformula = iformula,
      atomic_types = atomic_Ts}
   end
 
-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 is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+    (is_Const t orelse is_Free t) andalso
+    not (exists_subterm (curry (op =) t) u)
+  | is_legitimate_thf_def _ = false
+
+fun make_fact ctxt format type_enc iff_for_eq
+              ((name, stature as (_, status)), t) =
+  let
+    val role =
+      if is_type_enc_higher_order type_enc andalso status = Def andalso
+         is_legitimate_thf_def t then
+        Definition
+      else
+        Axiom
+  in
+    case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
+      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
+      if s = tptp_true then NONE else SOME formula
+    | formula => SOME formula
+  end
 
 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
   | s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
 (*
   | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t

              | _ => I)
           | _ => formula_fold (SOME (role <> Conjecture)) add_atom_eq_deps phi
         else
           I
       | add_eq_deps _ _ = I
-    fun has_status status (_, info) =
-      extract_isabelle_status info = SOME status
+    fun has_status status (_, info) = extract_isabelle_status info = SOME status
     fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
     val graph =
       Graph.empty
       |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
       |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem