diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Dec 18 16:11:53 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Dec 18 16:45:17 2000 +0100
@@ -61,9 +61,8 @@
 \isacommand{recdef} has been supplied with the congruence theorem
 \isa{map{\isacharunderscore}cong}:
 \begin{isabelle}%
-\ \ \ \ \ xs\ {\isacharequal}\ ys\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
+\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
 \end{isabelle}
 Its second premise expresses (indirectly) that the second argument of
 \isa{map} is only applied to elements of its third argument. Congruence