diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -19,7 +19,7 @@
 applies it automatically and the above definition of @{term"trev"}
 succeeds now. As a reward for our effort, we can now prove the desired
 lemma directly. The key is the fact that we no longer need the verbose
-induction schema for type @{name"term"} but the simpler one arising from
+induction schema for type @{text"term"} but the simpler one arising from
 @{term"trev"}:
 *};
 
@@ -39,7 +39,7 @@
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend to go through
 the chain of simplification steps in detail; you will probably need the help of
-@{name"trace_simp"}.
+@{text"trace_simp"}.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -66,7 +66,7 @@
 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
 (term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
-@{name"map_cong"}:
+@{thm[source]map_cong}:
 \begin{quote}
 @{thm[display,margin=50]"map_cong"[no_vars]}
 \end{quote}