diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Tue Jul 17 13:46:21 2001 +0200
@@ -14,7 +14,7 @@
 function was applied to an argument in its domain or not. If you do
 not need to make this distinction, for example because the function is
 never used outside its domain, it is easier to work with
-\emph{underdefined}\index{underdefined function} functions: for
+\emph{underdefined}\index{functions!underdefined} functions: for
 certain arguments we only know that a result exists, but we do not
 know what it is. When defining functions that are normally considered
 partial, underdefinedness turns out to be a very reasonable
@@ -143,9 +143,9 @@
 subsubsection{*The {\tt\slshape while} Combinator*}
 
 text{*If the recursive function happens to be tail recursive, its
-definition becomes a triviality if based on the predefined \isaindexbold{while}
+definition becomes a triviality if based on the predefined \cdx{while}
 combinator.  The latter lives in the Library theory
-\isa{While_Combinator}, which is not part of @{text Main} but needs to
+\thydx{While_Combinator}, which is not part of @{text Main} but needs to
 be included explicitly among the ancestor theories.
 
 Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}