mp_then: Make Pat selector backtrack over possible parses

With regression test.

Closes #567

Fix an mp_then/Pat selector bug

Include some more selftests. Thanks to Ramana for the bug report.

Fixes for mp_then/drule bug found in previous commit

Provide more test-cases as well. Extend normalisation done by
goal_assum after a theorem is returned to it after "resolution".

Fix mp_then bug: its PART_MATCH variant wasn't instantiating types

(It has a PART_MATCH variant in order to make sure preserve universal
quantification of variables that don't get specialised to make the
match happen.)

Fix over-aggressive normalisation in goal_assum

In particular, it's important that

P1 /\ P2 /\ ... Pn ==> F

stays as an implication and not turned into a negation.

Add test for expected behaviour with some instantiation provided by
mp_then.

Improve mp_then to eliminate matched preconditions

Make mp_then compile under Moscow ML

Write general imp_res_tac-like tool for combining thms