= Solution
Assuming `p` is an ordinary total Boolean predicate, replace success by `true` and the search's failure exception by `false`:
``
fun gordonPlain p Lf = true
| gordonPlain p (Br (x, left, right)) =
p x andalso
(gordonPlain p left orelse gordonPlain p right);
``
The <Standard ML> handler in the printed function belongs to the `else` expression: it tries the left subtree and, only if that search raises `Blair`, tries the right. It does not catch a failing label test at the current node. This scope follows the https://smlfamily.github.io/sml97-defn.pdf[Standard ML grammar, Appendix B]. Short-circuit `andalso` rejects the current label before visiting either child; short-circuit `orelse` visits the right child only after the left search fails. <Structural induction> on the <binary tree> proves that `tony` returns `true` exactly when `gordonPlain` does, and otherwise raises the exception converted by `gordon` to `false`. \b[The exception-free test is the root predicate conjoined with the disjunction of the two subtree tests.]
The total-predicate assumption matters: if `p` itself raises `Blair`, the original handler can catch it, whereas an implementation with no <exception handling> cannot in general convert that event to a Boolean result. The displayed replacement implements the intended Boolean tree property, not an exception-catching wrapper for arbitrary exceptional predicates.
Back to article page
