Use the Unicode turnstile (user-customizable) when printing theorems

When the trace “Unicode” is changed to 1 or 0 the theorem prefix is set to “⊢”
or the ASCII approximation “|-”, respectively. The prefix and suffix (empty by
default) can be customized via Globals.{thm_pp_prefix,thm_pp_suffix}.

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

Started moving EmitML code out of source scripts and into a single source
script "libraryScript.sml" in src/emitScript, adding calls to emitCAML
alongside the emitML calls in libraryScript.sml.

Minor changes and bugfixes to ML code generation. Have renamed
EmitML.exportML to EmitML.emitML, since exportML is used in
SML/NJ to dump the image. Also renamed Globals.exportMLPath
to Globals.emitMLDir (since it's a directory and not a path).

Also fixed bug in code generated for constructors and tuples.

New control variables.

Revised exportML so that it takes a path parameter, which tells
where the ML corresponding to a theory is to be written.

This has been propagated to all the theories that already export
ML, and the mkword.exe tool has been upgraded to also take a
path where it should write the generated ML. This is useful,
because doing an exportML to the same directory as the theory
files will end up confusing Holmake.

Fix for soundness bug; Globals.old changes its behaviour, and is no longer
a reference. It is used in the kernel to do semantically significant things
so can't just be left to a user to change arbitrarily.

Pretty significant "refactoring" of the early source code. All the stuff
that was in common between 0 and experimental-kernel moves into a new
prekernel directory. This can be thought of as the kernel utilities
directory, full of code that is not quite portableML because it's fairly
HOL specific, but that isn't really part of the core implementation of
types, terms and theorems.
(Also add a new pair_compare function to Lib.)