diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Nov 01 20:20:19 2007 +0100
@@ -1841,7 +1841,7 @@
 \label{sec:THEN}
 
 Let us reproduce our examples in Isabelle.  Recall that in
-{\S}\ref{sec:recdef-simplification} we declared the recursive function
+{\S}\ref{sec:fun-simplification} we declared the recursive function
 \isa{gcd}:\index{*gcd (constant)|(}
 \begin{isabelle}
 \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
@@ -2473,7 +2473,7 @@
 %
 We use induction: \isa{gcd.induct} is the
 induction rule returned by \isa{recdef}.  We simplify using
-rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the
+rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the
 definition of \isa{gcd} can loop.
 \begin{isabelle}
 \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\