Lambda the Ultimate

Hi,
I am looking everywhere for the proofs of the correctness and completeness of the Hindley-Milner type inference algorithm.

I could only find this short paper,
Principal type-schemes for functional program, by Damas and Milner, which gives only sketches of the proofs, and inform the reader that the detailed proofs are in Damas's Ph.D. thesis, titled Type Assignment in Programming Language, that I cannot find anywhere.

I would be grateful if anyone could point me to these proofs.

R.K.