diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -178,9 +178,9 @@
 \begin{isamarkuptext}%
 If the recursive function happens to be tail recursive, its
 definition becomes a triviality if based on the predefined \cdx{while}
-combinator.  The latter lives in the Library theory
-\thydx{While_Combinator}, which is not part of \isa{Main} but needs to
-be included explicitly among the ancestor theories.
+combinator.  The latter lives in the Library theory \thydx{While_Combinator}.
+% which is not part of {text Main} but needs to
+% be included explicitly among the ancestor theories.
 
 Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
 and satisfies the recursion equation \begin{isabelle}%