diff -r bbed9f218158 -r d3c0734059ee src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Oct 24 22:05:57 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Oct 25 15:31:58 2024 +0200
@@ -49,9 +49,11 @@
   val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
     (string * stature) list
   val atp_proof_prefers_lifting : string atp_proof -> bool
+  val is_lam_def_used_in_atp_proof : string atp_proof -> bool
   val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
   val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
     ('a, 'b) atp_step
+  val uncombine_term : theory -> term -> term
   val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format ->
     ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
     int Symtab.table -> string atp_proof -> (term, string) atp_step list
@@ -573,6 +575,9 @@
   (is_axiom_used_in_proof is_combinator_def atp_proof,
    is_axiom_used_in_proof is_lam_lifted atp_proof) = (false, true)
 
+val is_lam_def_used_in_atp_proof =
+  is_axiom_used_in_proof (is_combinator_def orf is_lam_lifted)
+
 val is_typed_helper_name =
   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix