diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Thu Nov 29 21:12:37 2001 +0100
@@ -146,9 +146,9 @@
 
 text{*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 @{text 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 @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
 and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}