Make resolve_then try harder to keep assumptions "in order"

In particular, when resolving p1 ... pn ==> qj against q1 ... qm ==> r
the result will be

p1 ... pn q1 ... q{j-1} q{j+1}...q{m} ==> r

modulo the fact that unification may cause assumptions to become the
same (duplicates are eliminated), either as each other, or as an
existing hypothesis. This makes the proposed irule (goal_assum o
resolve_then Any mp_tac) behave a bit more like MATCH_MP_TAC, rather
than as currently.

Fix a resolve_then bug when the goal should be completely solved

Fix resolve_then so that it compiles under Moscow ML

Implement a unification-based version of mp_then with similar API

Documentation and concrete instantiations (à la drule etc) of the
underlying primitive still to come.