diff -r efee34ff4764 -r 6a98d0826daf doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jul 23 14:39:21 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jul 23 15:04:56 2007 +0200
@@ -602,7 +602,7 @@
   | MPair  [intro]:
               "\<lbrakk>X \<in> synth H;  Y \<in> synth H\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:
-              "\<lbrakk>X \<in> synth H;  Key(K) \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
+              "\<lbrakk>X \<in> synth H;  Key K \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
 (*<*)
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   by (auto, erule synth.induct, auto)