--- a/doc-src/TutorialI/Misc/Itrev.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Mon May 02 11:03:27 2005 +0200
@@ -119,7 +119,7 @@
those that change in recursive calls.
A final point worth mentioning is the orientation of the equation we just
-proved: the more complex notion (@{term itrev}) is on the left-hand
+proved: the more complex notion (@{const itrev}) is on the left-hand
side, the simpler one (@{term rev}) on the right-hand side. This constitutes
another, albeit weak heuristic that is not restricted to induction:
\begin{quote}