Fix more missing ERR definitions

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.

Get ARM examples to build; v7-step regression fails though

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.

Overhaul to rich_listTheory (it had become a bit of a disaster area).

Some points:

1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN.

2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them.

3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g.

val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ
val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC

4. Some incompatibilities are introduced:

* FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT.
* COUNT_LIST___ADD -> COUNT_LIST_ADD
* COUNT_LIST___COUNT -> COUNT_LIST_COUNT
* The compute theorems for COUNT_LIST and SPLITP have been renamed.
* Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT

5. Some theorems in listTheory have gained quantifiers.

Get ARM/v4's user-printer to compile again.

adaption to the changes to userprinter

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Fix required after changes to add_user_printer.

Minor changes.

Renamed bsubst to update (as it is in v4T).

Moved a few definitions/theorems to better homes.

Misc. fixes to remove Mosml specific features.

examples/elliptic/arm -> examples/ARM/v4
examples/arm6 -> examples/ARM/arm6-verification