src/HOL/Tools/ATP/atp_problem_generate.ML

       | freeze (Var ((s, i), T)) =
         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun unextensionalize_def t =
-  case t of
-    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
-    (case strip_comb lhs of
-       (c as Const (_, T), args) =>
-       if forall is_Var args andalso not (has_duplicates (op =) args) then
-         @{const Trueprop}
-         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
-            $ c $ fold_rev lambda args rhs)
-       else
-         t
-     | _ => t)
-  | _ => t
-
 fun presimp_prop ctxt type_enc t =
   let
     val thy = Proof_Context.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
               |> transform_elim_prop

   in
     {name = name, stature = stature, role = role, iformula = iformula,
      atomic_types = atomic_Ts}
   end
 
-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
+         is_legitimate_tptp_def t then
         Definition
       else
         Axiom
   in
     case t |> make_formula ctxt format type_enc iff_for_eq name stature role of

 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (role, t)) =>
           let
             val role =
               if is_type_enc_higher_order type_enc andalso
-                 role <> Conjecture andalso is_legitimate_thf_def t then
+                 role <> Conjecture andalso is_legitimate_tptp_def t then
                 Definition
               else
                 role
           in
             t |> role = Conjecture ? s_not