It turns out - or so I'm told, I must admit to never working through the details - that parts of the proof can be abstracted, and from this point of view a key ingredient (implicit or explicit in the proof, according to taste) is the vanishing of a certain $\varprojlim_1$ \lim_1$group -- as assured by the "abstract" ML-theorem that you mention. I'm not sure where this was first recorded - I hesitate to say "folklore" since that's just another way of saying "don't really know am and not a historian". One place this is discussed is in Runde's book A taste of topology: see Google Books for the relevant part. IIRC, Runde says that the use of the "abstract" Mittag-Leffler theorem to prove the "classical" one, and to prove things like the Baire category theorem, can be found in Bourbaki. Perhaps someone better versed in the mathematical literature (or at least better versed in the works of Bourbaki) can confirm or refute this? 1 The wording of your question suggests that you're familiar with the "classical" Mittag-Leffler theorem from complex analysis, which assures us that meromorphic functions can be constructed with prescribed poles (as long as the specified points don't accumulate in the region). It turns out - or so I'm told, I must admit to never working through the details - that parts of the proof can be abstracted, and from this point of view a key ingredient (implicit or explicit in the proof, according to taste) is the vanishing of a certain$\varprojlim_1\$ group -- as assured by the "abstract" ML-theorem that you mention.