diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Recdef/examples.thy
--- a/doc-src/TutorialI/Recdef/examples.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -69,7 +69,7 @@
 *}
 consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
 recdef sep2 "measure length"
-  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
+  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
   "sep2 xs       = (\<lambda>a. xs)";
 
 text{*