diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -26,9 +26,9 @@
 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
 \end{quote}
 where @{term"set"} returns the set of elements of a list (no special
-knowledge of sets is required in the following) and @{name"term_list_size ::
+knowledge of sets is required in the following) and @{text"term_list_size ::
 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
-(when @{name"term"} was defined).  First we have to understand why the
+(when @{text"term"} was defined).  First we have to understand why the
 recursive call of @{term"trev"} underneath @{term"map"} leads to the above
 condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
 will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above