ML has a sophisticated exception --handling facility. Certain functions yield runtime errors on certain arguments and are therefore said to fail on these arguments. The result of a failure is a token, usually the function name. The token returned by a failure can be specified by using the construct failwith in a fashion to be described later.
A special operator allows one to ``catch'' failures. The combination has the value unless results in a failure, in which case it has the value of . As we shall see, the exception--trap mechanism is useful in writing tactics.