semi-major change: separate instance-matching from the constant assignment

this helps require constant assignments to be "uniform" on polymorphic
values. now the term semantics depends on the signature. this is closer
to what RDA has done, although it seems we need a small fix to his
approach to prevent constant assignments depending on irrelevant
valuations of type variables. holSoundnessScript.sml not updated in this
commit.