Fix for a Define bug spotted by mjcg. When
dealing with recursive calls under a case,
if variables with certain names (those
starting with v) are bound in the case
pattern then it can happen that variables
generated during pattern matching can be
the same, leading to failed proofs. Totally
obscure, and dealt with properly (I think)
in normal pattern matching. So, a difference
between Pmatch and Functional. The fix is
to invent a class of variables not accepted
by the parser (i.e. starting *v) and to later eliminate
the weird names from any theorems coming out of Hol_defn.

Some other trivial mods made in passing also, plus
tests for the new behaviour.

Also a new conversional, MAP_THM, which applies the
given conversion to the assumptions and conclusion
of the given theorem.

Mods to get examples working again.

CASE_TAC no longer worked since I added
non-datatype entries to the TypeBase.
That has been fixed, and better error
messages are now generated from some
of the entrypoints in TypeBase that
expect datatypes.

Also fixed some rotted proofs in
tfl/examples.

Updating some examples, and adding a variation on dfs, where
the graph has a function type but type system nonetheless
ensures that the graph is finite.

Minor changes.

Minor changes?

Incremental changes to regexp stuff.

Adding a fast regular expression matcher. Changing old regexp.sml
to live in regexp.naive