diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Misc/Itrev.thy
--- 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}