diff -r 6f2951938b66 -r 7648ac4a6b95 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jan 04 19:23:28 2002 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jan 04 19:24:43 2002 +0100
@@ -97,7 +97,7 @@
 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
 Embedded in this syntax are the types and formulae of HOL, whose syntax is
-extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
+extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
 To distinguish the two levels, everything
 HOL-specific (terms and types) should be enclosed in
 \texttt{"}\dots\texttt{"}.