Update the semantics of pattern matching.

Now falling off the end of a match is a type error, rather than a Bind
error or a re-raise (for case and handle resp.). The translation to IL2,
at the moment, always adds a default case, but of course we'll want to
improve that with detection of (at least some) exhaustive matches.

The proofs aren't updated.