Slightly tweak TeX tools' Holmakefile further

* Use ifdef to hide Poly/ML specific command from Moscow ML (strictly
  unnecessary but tidier)
* Use hol.builder rather than hol.builder0 in Poly/ML's creation of an
  intermediate object file.  This is for the sake of speed.