diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/GCD.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -2851,7 +2851,7 @@
 definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat" 
   where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
 
-syntax "_type_char" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>prefix CHAR\<close>\<close>CHAR/(1'(_')))\<close>)
+syntax "_type_char" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>mixfix CHAR\<close>\<close>CHAR/(1'(_')))\<close>)
 syntax_consts "_type_char" \<rightleftharpoons> semiring_char
 translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
 print_translation \<open>