diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Thu Aug 09 18:12:15 2001 +0200
@@ -281,7 +281,7 @@
 @{text"case"}-expressions, as it does @{text"if"}-expressions, 
 because with recursive datatypes it could lead to nontermination.
 Instead, the simplifier has a modifier
-@{text split}\index{*split (modified)} 
+@{text split}\index{*split (modifier)} 
 for adding splitting rules explicitly.  The
 lemma above can be proved in one step by
 *}