fix some evaluate' inductions in ml_translatorScript.sml

because the type of evaluate_match has changed.

this commit doesn't fix everything in ml_translatorScript.sml: the next
theorem concerning evaluate_match' concludes that Bind_error is never
raised, but Bind_error doesn't exist any more (or rather, it is a normal
value that could be raised by the user, so we can't prove it's never
raised). will try weakening the conclusion to see what else breaks...