diff -r 07b13770c4d6 -r e0ab13bec5c8 doc-src/TutorialI/Recdef/examples.thy
--- a/doc-src/TutorialI/Recdef/examples.thy	Tue Feb 20 10:37:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Feb 20 11:27:04 2001 +0100
@@ -57,8 +57,11 @@
   "sep1(a, xs)     = xs";
 
 text{*\noindent
-This defines exactly the same function as @{term"sep"} above, i.e.\
-@{prop"sep1 = sep"}.
+To guarantee that the second equation can only be applied if the first
+one does not match, Isabelle internally replaces the second equation
+by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
+@{prop"sep1(a, [x]) = [x]"}.  Thus the functions @{term sep} and
+@{term sep1} are identical.
 
 \begin{warn}
   \isacommand{recdef} only takes the first argument of a (curried)