Remove parmonadsyntax's dependency on state_transformerTheory

Restore ppstream_funs as nullary type operator in term_pp_types

This name is used in user-written code (users' special purpose
pretty-printers), and there is no reason to rebind this name, forcing
them to change things.

Fix TeX code to compile- some tests still not passing

Absyn post-processors now see the current grammar

User pp fns can note terms as binders to system printer

This allows better behaviour in a test case shown to me by Mike, where
annotations in monad-syntax weren't appearing.

Make monadsyntax more flexible with monad_unitbind

Previously, one had to bind "monad_unitbind" to a real constant, such as
option$OPTION_IGNORE_BIND. Now one can bind to a pattern, such as

\m1 m2. OPTION_BIND m1 (K m2)

This means that one doesn't have to define as many constants when
working with a fresh monad, which feels like an advantage.

Also clean-up monad selftest, and test new behaviour.

Some minor fixes to TeX hacking for monad syntax.

In short, spaces shouldn't appear in the "hol" field of TeX_notation
call because tokens with spaces in them aren't going to get omitted
if the grammar rule is remotely sensible (math mode munging gets hard
if there are literal spaces around). Putting spaces into the TeX
field is wrong (even wronger, really) for the same reason.

TeX notation for monad syntax

I thought I had done this before but apparently not. Make do and od
keywords (this was already the case for parmonadsyntax, now it also
works for monadsyntax). Also, fix (I hope - correct if I'm wrong)
parmonadsyntax's length for the left arrow.

Move state_transformer stuff to its own directory src/monad.

This facilitates the addition of a FOR constant to state_transformerTheory.