diff -r f075640b8868 -r 3abf6a722518 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -102,7 +102,7 @@
 
 subsection \<open>The Kernel of a Ring Homomorphism\<close>
 
-\<comment>"the kernel of a ring homomorphism is an ideal"
+\<comment> \<open>the kernel of a ring homomorphism is an ideal\<close>
 lemma (in ring_hom_ring) kernel_is_ideal:
   shows "ideal (a_kernel R S h) R"
 apply (rule idealI)