The author deals with first-order TP without skolemization. He clearly
identifies (recalls) the problems raised by the skolemization rule and the
alternatives to its use. The goal of the paper is to provide bases for
inductive theorem proving.
I did not check all definitions and proofs. They seem correct.
In my opinion, this is a good, technical, well written paper.