diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/CodeGen/CodeGen.thy
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Jul 17 13:46:21 2001 +0200
@@ -110,8 +110,8 @@
 apply(induct_tac xs, simp, simp split: instr.split);
 (*<*)done(*>*)
 text{*\noindent
-Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
-be modified in the same way @{text simp} can. Thus the proof can be
+Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
+be modified in the same way as @{text simp}.  Thus the proof can be
 rewritten as
 *}
 (*<*)