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