--- a/src/CCL/Gfp.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/CCL/Gfp.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -10,7 +10,7 @@
 begin
 
 definition
-  gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> "greatest fixed point"
+  gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> \<open>greatest fixed point\<close>
   "gfp(f) == Union({u. u <= f(u)})"
 
 (* gfp(f) is the least upper bound of {u. u <= f(u)} *)