Fix TeX code to compile- some tests still not passing

New "raw" interface in EmitTeX with user-supplied maps from HOL to LaTeX.

The user-supplied maps are consulted first for information about HOL
tokens, and if they come up short, the built-in support is used.
Given how easy it is to redefine LaTeX commands, this is not likely to
be used to override the standard map (choice of variable name in code
notwithstanding), but will more likely allow the map to be extended.

Update to EmitTeX, following changes to pretty-printing in HOL.

Moving TeX.