should no longer refer to tr.  (This is useful for
inference rules like hyperresolution, which backtrack,
undoing parts of substitutions.)
<A NAME="unify"></A><HR><PRE><B>BOOL unify(<A HREF="term.html">Term</A> t1, <A HREF="unify.html">Context</A> c1,
	   <A HREF="term.html">Term</A> t2, <A HREF="unify.html">Context</A> c2, <A HREF="unify.html">Trail</A> *trp);
</B></PRE>This routine tries to unify two terms in their respective
contexts.  <A HREF="unify.html">Trail</A> * trp is the address of a <A HREF="uni