Now up to type pretty-printing

Link the type pretty-printer to the PPBackEnd infrastructure. In
Emacs, types are printed in italics, with tooltips indicating the real
nature of the underlying thing (type abbreviations supported).

Turns off bracket syntax for array types when using EmitML.

Added a substitute operation :+ for FCPs.

Also made EmitML work with numeric types e.g. ``:2`` gets the ML
type "unit bit0".

Implementation of "parse only" type abbreviations. The main function to
use is type_abbrev : (string * hol_type) -> unit

If the hol_type has type variables in it, then these become parameters to
the string, making it an abbreviation for a type operator. E.g.,
type_abbrev("set", ``:'a -> bool``)
allows you to write ``:num set``.

No attempt to pretty-print types in accordance with stored abbreviations,
so the system will spit back ``:num -> bool`` in response to this. (Hey,
if it's good enough for Moscow ML, it's good enough for us.)

Also split off type_grammars into their own source module.

Support for new representation of strings.Minor changes.

Added .sig file to type_pp.
Fixed bug which was pretty-printing :(bool |-> bool) |-> bool without any
parentheses.
Removed some spurious reference variables from term_pp.