src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

   type 'a problem = 'a ATP_Problem.problem
   type translated_formula
 
   val fact_prefix : string
   val conjecture_prefix : string
-  val translate_fact :
+  val translate_atp_fact :
     Proof.context -> (string * 'a) * thm
     -> term * ((string * 'a) * translated_formula) option
   val prepare_atp_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
     -> (term * ((string * 'a) * translated_formula) option) list

                  if exists is_needed ss then map baptize ths else [])) @
     (if is_FO then [] else map baptize mandatory_helpers)
     |> map_filter (Option.map snd o make_fact ctxt false)
   end
 
-fun translate_fact ctxt (ax as (_, th)) = (prop_of th, make_fact ctxt true ax)
+fun translate_atp_fact ctxt (ax as (_, th)) =
+  (prop_of th, make_fact ctxt true ax)
 
 fun translate_formulas ctxt full_types hyp_ts concl_t facts =
   let
     val thy = ProofContext.theory_of ctxt
     val (fact_ts, translated_facts) = ListPair.unzip facts