Move the match_position datatype from mp_then to its own file

This type will be used in the API to the forthcoming resolve_then.
Separating it out into a _dtype.sml file also avoids having to repeat
the datatype definition in .sig and .sml file.

Move mp_then.PART_MATCH' to Drule and document it

Expose mp_then's PART_MATCH' function

This one differs from PART_MATCH is that it keeps generalised
variables quantified if they're not involved in the match.

Fix type signature of mp_then in .sig

Provide mp_then with a signature

The documentation for mp_then does not appear in the auto-generated
HTML index. This seems to be because it has no signature. This adds
a signature for mp_then so that it becomes visible in the generated
HTML index.