Hey, you are right. the method I was thinking of does require model theory to justify its axioms (IST). It had been waved away as you put it, so that the core could be focused on. But you don't really need to understand why the axioms are justified any more than most people understand the axioms of ZFC (excepting those like you of course). And if the outcome is a better first intuition of calculus, I don't think it is accurate to label it a fly.

I did find out that there is a constructive approach though, so the axiom of choice is not actually necessary. www.math.ucla.edu/~asl/bsl/0403/0403-001.ps