ML two objects of type ` term` are equal if and only if they are
--convertible variants of each other. That is, they are equal if and
only if the
bound variables can be renamed so that the terms are identical. For objects
of type ` proof`, ` rule` and ` declaration`, two objects are equal
if and only if they are the * same* object.

Thu Sep 14 08:45:18 EDT 1995