Some parts in the paper from 1979 are fuzzy. Peter Dybjer has a clearer version available at
http://www.cse.chalmers.se/~peterd/papers/oplss15.html .
(These materials were made available in context of the Oregon programming languages summer school in 2015.)