What is a preterm parser?
Since HOL Light is based on $\lambda$ Calculus and HOL Light is typed and as we know there is untyped $\lambda$ Calculus and typed $\lambda$ Calculus, HOL Light starts by parsing something close to untyped $\lambda$ Calculus, creating pre-terms. Then it applies a typing checking and typing phase, along with resolving overloaded operators resulting is something closer to typed $\lambda$ Calculus. Obviously HOL is much more than typed $\lambda$ Calculus, but the point here is to understand what pre-term means with regards to parsing.

The only reference I have found for this is in  

Lectures on the Curry-Howard Isomorphism
Section 1.2 Pre-terms and $\lambda$-terms.

Specifically how this is done in HOL Light is in the parser module:

The pre-terms are created with

let ptm = (parse_pteterm &lt;&lt; lex &lt;&lt; explode) input


and the type checking, etc. is done with 

let term = (term_of_preterm &lt;&lt; (retypecheck [])) ptm