Remove eqtype declaration for term type

Rename match_all_tac to first_match_tac

The new name is less confusing, given what it does.
Arguably it does not need to be bound at all, since the implementation
is so simple.

Add two values to the Streams module, from match_goal

Simplify match_goal.sig

So there is only one main signature in the file, to make things easier
with Moscow ML, as suggested by Michael.

Remove string-based encoding of names, tidy signature

The preferred approach to creating matchers is via the mg structure, so
there is no need for a hacky string-based approach to short names.

Add an initial implementation of match_goal

This is a tactic builder that does automatic logic-programming-style
search over (sub)terms in the assumptions and conclusion of a goal
ensuring certain patterns match and that a given tactic (which can refer
to the terms and assumptions named by the pattern) succeeds.

Work with Jack Gallagher, and inspired by a similar facility in Coq.