Use Const annotations in the TeX pretty-printing backend.

Intention is to allow users to redefine \HOLConst to set their
constant names in something other than the default \texttt.
Make constant annotations appear in more places when pretty-printing.

This affects the TeX selftests, which now see those \HOLConst
annotations (as desired).
The boss/theory_tests can be done with the boss heap.

Move it to after the [poly]bin/hol build-sequence directive to have
this happen.