TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't — whether you deal with (higher-order) logics or 𝜆-calculus. They're so subtle that binding representations form an open research field, with a competition (the POPLmark challenge) some years ago. There are even jokes by people in the field about the complexity of approaches to binding.
So, if you care about metamathematics (and most mathematicians don't), you need to deal with binding. But many mathematicians can safely treat the formalization of binding as if it were a "foundational" problem.
Another point is that binding was the only "new" problem in languages with higher-order functions, because the theory of languages with binding is just algebra (for constants) + binding. Mitchell's "Foundations of Programming Languages" actually presents things in this order and is rather enlightening.
I'm aware of how his work paved way for λ-calculus and the impact of "it" on computing and functional programming in general. My question is mostly directed to the time "prior" to the creation of λ-calculus and "after" Schönfinkel's paper.
I must be missing something, but this remark seems to make no difference. Binding in higher-order logics and binding in λ-calculus seem as hard, so as long as people cared about higher-order logics, they had to deal with binding. I'm biased by using Curry-Howard-isomorphism-based theorem provers that implement logic by simply implementing a type theory (where types are formulas and programs are proof terms), so that I just deal with binding once.
On the other hand, IIRC, at the time indeed few cared about Schönfinkel's work — partly because of how he (didn't) publish it — the papers were mostly written by colleagues based on the research he did (see here, page 4); Curry then rediscovered the theory independently.
Caveat: I'm not an historian, but a PhD student in PL, so mine is a modern (and hopefully accurate) perspective on the topic.
EDIT:
Why is binding subtle, a bit more concretely
There are two facets to it — first, implementing it is hard. Secondly, metamathematics is the mathematics of proof manipulation: this manipulation is typically automatic, that is, it's an algorithm — so essentially, you face all the difficulties of implementation, plus making proofs about them. Below I give examples. The examples have a modern perspective — they are about actually formalized proofs. However, some of the difficulties would extend to accurate manual proofs — as long as you don't cheat on details.
This shows that Schönfinkel simply gave the first solution to this problem, but this was far from definitive.
Implementing it is subtle because of shadowing
The basic problem in implementation is shadowing. Usually one doesn't reuse the same name for different bound variables. But you can't avoid it in lambda calculus, at least because functions (and their bound variables) are duplicated: $(\lambda f. f~1 + f~2) (\lambda x . x)$ reduces to $(\lambda x . x)~1 + (\lambda x . x)~2$. This isn't a problem yet, but starting from $(\lambda f x. f (f x))\ (\lambda g y . g~y)\ z$ gives you $(\lambda g y . g~y)\ (\lambda g y . g~y)\ z$ and then $(\lambda y . (\lambda g y . g~y)~y)\ \ z$: now you need to deal with shadowing. You can avoid this, at the cost of complicating the beta-reduction rule.
Once you have different variables with the same name, you also need to prevent capture. The simplest example of capture is that applying the function $\lambda x y. x$ (return first argument) to $y$ must not give $\lambda y. y$ (the identity function), but $\lambda y'. y$ (a constant function).
What's worse is that the counterexamples to naive algorithms are hard to construct when you know the problem already, let alone when you don't. Bugs in almost correct algorithms often lie undetected for years. I hear that even good students typically fail to come up (on their own) with the correct definition of capture-avoiding substitution. In fact, PhD students (me included) and professors aren't exempt from these problem.
That's one reason why some (including one of the best textbooks on programming languages, Types and Programming Languages by Benjamin Pierce) recommend nameless representation (not quite combinatory logic, even though it has been used, but rather deBrujin indexes).
Proofs about it are subtle
It turns out that proofs about binding are no simpler than the implementation, as mentioned above. Of course, correct algorithms exist, and proof about them exist — but without advanced machinery, for each language using binding you need to repeat the proofs, and those proofs are simply very big and annoying if you use the definitions for binding on pen and paper.
To exemplify algorithms involved in metamathematics, consider the deduction theorem in logics, that allows composing a proof of $B$ assuming $A$ and a proof of $A$ to get a proof of $B$. To prove that theorem, you actually exhibit an algorithm that works on the syntax of the two proofs involved and produces the syntax for a proof of $B$. This algorithm needs to deal with binding.
Next, I looked up my best example of "what goes wrong if you try formalizing the standard definition". Russell O’Connor (who's on this site) formalized the first Gödel's incompleteness theorem in Coq (a theorem prover of the kind mentioned above) — and that theorem involves a logic (with all the relevant algorithms) in another logic (with the syntax of the first logic coded as numbers). He used the definitions which are used on paper and formalized them directly.
Search for "substitution" or "variable" and count how often they appear in reference to problems to get an impression.
http://r6.ca/Goedel/goedel1.html
I never use those definitions in my work, but each alternative approach has some downside.
