Ah, Thomas Forster's 1998 paper "Weak systems of set theory related to HOL" is available on-line at various places including https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps
He says it is proved in
Jensen RB "On the consistency of a slight (?) modification of Quine's NF" Synthese 19 1969 pp 25--63.
Lake J "Comparing Type theory and Set theory" Zeitschrift fur Matematische Logik 21 1975 pp 355-56.
For a fanatically detailed proof and discussion see Mathias at https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf
