--- a/doc-src/Ref/substitution.tex Mon Mar 21 10:51:28 1994 +0100
+++ b/doc-src/Ref/substitution.tex Mon Mar 21 11:02:57 1994 +0100
@@ -141,7 +141,7 @@
function {\tt dest_eq} requires knowledge of Isabelle's representation of
terms. For {\tt FOL} it is defined by
\begin{ttbox}
-fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u);
+fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u)
\end{ttbox}
Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
\hbox{\tt op =} is the internal name of the infix operator~{\tt=}.