# HG changeset patch
# User wenzelm
# Date 754233400 -3600
# Node ID 67d046de093ee5219af6569a0a6a53de91871036
# Parent  e8d8fa0ddcef3b11f355e5499cdcaabdea2abec3
corrected trivial typo;

diff -r e8d8fa0ddcef -r 67d046de093e doc-src/Ref/substitution.tex
--- a/doc-src/Ref/substitution.tex	Thu Nov 25 13:54:21 1993 +0100
+++ b/doc-src/Ref/substitution.tex	Thu Nov 25 14:16:40 1993 +0100
@@ -143,7 +143,7 @@
 \begin{ttbox} 
 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
+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=}.
 Pattern-matching expresses the function concisely, using wildcards~({\tt_})
 to hide the types.