In Extending Sledgehammer with SMT solvers there is this claim:
Lambda-abstractions are rewritten to Turner combinators or transformed into explicit functions using lambda-abstractions.
The linked reference, Translating higher-order clauses to first-order clauses does not clarify how are this method synchronized. Do we use both of them always? Is one preferred to the other?
According to mediatum.ub.tum.de/doc/1097834/1097834.pdf the choice of method is tailored for each prover.