I think in the background of article's premises is an argument about classical vs. intuitionistic logic, rather than only about the merits of putting stuff in the kernel vs. outside.

Isabelle seems to use classical logic and set theory. Classical logic is often simpler, but when you do the "hard toil" (as the article puts it) of building recursive functions on set theory, all you've really done is to nonconstructively prove the existence of a set of pairs with certain properties. Good luck evaluating such an abstract "existence" with any concrete argument. Whereas intuitionistic logic as used by Coq is more complicated, but that's in part because its notion of "function" is an actual procedure in your computer that can accept an argument and produce a result.

At least that's to the best of my understanding; it's been a while since I have looked at any of this, so feel free to make corrections.