src/HOL/Algebra/Multiplicative_Group.thy

--- a/src/HOL/Algebra/Multiplicative_Group.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -144,7 +144,7 @@
   where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
 
 notation (latex output)
-  phi' ("\<phi> _")
+  phi' (\<open>\<phi> _\<close>)
 
 lemma phi'_nonzero:
   assumes "m > 0"