diff -r 9e1136e8bb1f -r 7695e4de4d86 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 15:37:32 2010 +0100
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 16:04:22 2010 +0100
@@ -30,7 +30,7 @@
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend that you go through
 the chain of simplification steps in detail; you will probably need the help of
-@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
+@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\