diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Rings.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -1273,7 +1273,7 @@
     and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
     and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
     and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
-  -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
+  \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
   
 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
   fixes normalize :: "'a \<Rightarrow> 'a"