src/HOL/Algebra/Divisibility.thy

--- a/src/HOL/Algebra/Divisibility.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -1909,7 +1909,7 @@
 qed
 
 
-\<comment> \<open>A version using @{const factors}, more complicated\<close>
+\<comment> \<open>A version using \<^const>\<open>factors\<close>, more complicated\<close>
 lemma (in factorial_monoid) factors_irreducible_prime:
   assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"
   shows "prime G p"