Make the TeX munger correctly depend on the mungeTools module.
Fix munger bug where math-mode option conflicted with var-substitutions

In particular, something like

  \HOLthm[m/x]{theorem-name}

was parsed as an attempt to set the math-mode spacing to /x instead of
as a substitution of name m for name x.