Allow specification of grammar to LaTeX munger commands

[mn200]

E.g., something like

\HOLtm[g=bool]{x + y}

would cause the printing of a term like

arithmetic$+ x y

as the bool grammar has no knowledge of the + constant.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.