diff -r f075640b8868 -r 3abf6a722518 src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -73,7 +73,7 @@
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs
                       | Notes A X  => parts {X} \<union> used evs)"
-    \<comment>\<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
+    \<comment> \<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
         follows @{term Says} in real protocols.  Seems difficult to change.
         See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}.\<close>