Danvy & Nielsen’s one-pass CPS transform has a straightforward definition, but clashes between the names of variables it introduces make it difficult to mechanically prove correct. Existing mechanical proofs either side-step the issue by using nameless representations, or rely on tedious \(\alpha \) -equivalence relations between target terms. This paper presents a new formulation of the transform using evaluation contexts that allows deterministic introduction of fresh names, eliminating the need to work up to \(\alpha \) -equivalence. We use our formulation to present a new and straightforward simulation proof of the correctness of the one-pass CPS transform, which we have mechanised in the HOL4 theorem prover.