diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Oct 09 19:20:55 2000 +0200
@@ -75,10 +75,10 @@
 The fact that substitution distributes over composition can be expressed
 roughly as follows:
 \begin{isabelle}%
-\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
+\ \ \ \ \ subst\ {\isacharparenleft}f\ {\isasymcirc}\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
 \end{isabelle}
 Correct this statement (you will find that it does not type-check),
-strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
+strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition;
 its definition is found in theorem \isa{o{\isacharunderscore}def}).
 \end{exercise}
 \begin{exercise}\label{ex:trev-trev}