diff -r 2f831a45d571 -r 245b64afefe2 doc-src/Ref/substitution.tex
--- a/doc-src/Ref/substitution.tex	Fri Dec 05 17:31:01 1997 +0100
+++ b/doc-src/Ref/substitution.tex	Fri Dec 05 18:44:56 1997 +0100
@@ -78,7 +78,7 @@
 assumption~$c=a$, since $c$ does not occur in~$a=b$.  Of course, we can
 work out a solution.  First apply {\tt eresolve_tac\ts[subst]\ts\(i\)},
 replacing~$a$ by~$c$:
-\[ \List{c=b} \Imp c=b \]
+\[ c=b \Imp c=b \]
 Equality reasoning can be difficult, but this trivial proof requires
 nothing more sophisticated than substitution in the assumptions.
 Object-logics that include the rule~$(subst)$ provide tactics for this