diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Enum.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -497,7 +497,7 @@
 datatype (plugins only: code "quickcheck" extraction) finite_1 =
   a\<^sub>1
 
-notation (output) a\<^sub>1  ("a\<^sub>1")
+notation (output) a\<^sub>1  (\<open>a\<^sub>1\<close>)
 
 lemma UNIV_finite_1:
   "UNIV = {a\<^sub>1}"
@@ -601,8 +601,8 @@
 datatype (plugins only: code "quickcheck" extraction) finite_2 =
   a\<^sub>1 | a\<^sub>2
 
-notation (output) a\<^sub>1  ("a\<^sub>1")
-notation (output) a\<^sub>2  ("a\<^sub>2")
+notation (output) a\<^sub>1  (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2  (\<open>a\<^sub>2\<close>)
 
 lemma UNIV_finite_2:
   "UNIV = {a\<^sub>1, a\<^sub>2}"
@@ -730,9 +730,9 @@
 datatype (plugins only: code "quickcheck" extraction) finite_3 =
   a\<^sub>1 | a\<^sub>2 | a\<^sub>3
 
-notation (output) a\<^sub>1  ("a\<^sub>1")
-notation (output) a\<^sub>2  ("a\<^sub>2")
-notation (output) a\<^sub>3  ("a\<^sub>3")
+notation (output) a\<^sub>1  (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2  (\<open>a\<^sub>2\<close>)
+notation (output) a\<^sub>3  (\<open>a\<^sub>3\<close>)
 
 lemma UNIV_finite_3:
   "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3}"
@@ -971,10 +971,10 @@
 datatype (plugins only: code "quickcheck" extraction) finite_4 =
   a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
 
-notation (output) a\<^sub>1  ("a\<^sub>1")
-notation (output) a\<^sub>2  ("a\<^sub>2")
-notation (output) a\<^sub>3  ("a\<^sub>3")
-notation (output) a\<^sub>4  ("a\<^sub>4")
+notation (output) a\<^sub>1  (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2  (\<open>a\<^sub>2\<close>)
+notation (output) a\<^sub>3  (\<open>a\<^sub>3\<close>)
+notation (output) a\<^sub>4  (\<open>a\<^sub>4\<close>)
 
 lemma UNIV_finite_4:
   "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4}"
@@ -1060,11 +1060,11 @@
 datatype (plugins only: code "quickcheck" extraction) finite_5 =
   a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
 
-notation (output) a\<^sub>1  ("a\<^sub>1")
-notation (output) a\<^sub>2  ("a\<^sub>2")
-notation (output) a\<^sub>3  ("a\<^sub>3")
-notation (output) a\<^sub>4  ("a\<^sub>4")
-notation (output) a\<^sub>5  ("a\<^sub>5")
+notation (output) a\<^sub>1  (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2  (\<open>a\<^sub>2\<close>)
+notation (output) a\<^sub>3  (\<open>a\<^sub>3\<close>)
+notation (output) a\<^sub>4  (\<open>a\<^sub>4\<close>)
+notation (output) a\<^sub>5  (\<open>a\<^sub>5\<close>)
 
 lemma UNIV_finite_5:
   "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}"