diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -61,9 +61,7 @@
 
 txt{*\noindent
 Unfortunately, this is not a complete success:
-\begin{isabelle}\makeatother
-~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
-\end{isabelle}
+@{subgoals[display,indent=0,margin=65]}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
 @{term"[]"}. The corresponding heuristic: