--- a/src/HOL/IMP/Star.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/IMP/Star.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -7,7 +7,7 @@
 refl:  "star r x x" |
 step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
 
-hide_fact (open) refl step  \<comment>"names too generic"
+hide_fact (open) refl step  \<comment> \<open>names too generic\<close>
 
 lemma star_trans:
   "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"