--- a/src/Doc/Sugar/Sugar.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/Doc/Sugar/Sugar.thy Tue Jan 16 09:30:00 2018 +0100
@@ -455,7 +455,7 @@
\<close>
lemma True
proof -
- \<comment> "pretty trivial"
+ \<comment> \<open>pretty trivial\<close>
show True by force
qed
text_raw \<open>