diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Thu May 12 17:17:57 2011 +0200
@@ -32,7 +32,7 @@
 the matching private key, and vice versa:
 *}
 
-types key = nat
+type_synonym key = nat
 consts invKey :: "key \<Rightarrow> key"
 (*<*)
 consts all_symmetric :: bool        --{*true if all keys are symmetric*}