doc-src/TutorialI/Datatype/document/Nested.tex

 Correct this statement (you will find that it does not type-check),
 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}
-  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term}
+  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term}
 that recursively reverses the order of arguments of all function symbols in a
   term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
 \end{exercise}
 
 The experienced functional programmer may feel that our definition of