diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Protocol/document/Message.tex
--- a/doc-src/TutorialI/Protocol/document/Message.tex	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Protocol/document/Message.tex	Thu May 12 17:17:57 2011 +0200
@@ -47,7 +47,7 @@
 the matching private key, and vice versa:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{types}\isamarkupfalse%
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
 \ key\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
 \isacommand{consts}\isamarkupfalse%
 \ invKey\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}key\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}%