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