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.