diff -r 0c898f7d9b15 -r 9e2eb05cc2b7 src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Oct 05 15:18:49 2024 +0200
+++ b/src/HOL/String.thy	Sat Oct 05 22:24:24 2024 +0200
@@ -224,7 +224,7 @@
 type_synonym string = "char list"
 
 syntax
-  "_String" :: "str_position \<Rightarrow> string"    (\<open>_\<close>)
+  "_String" :: "str_position \<Rightarrow> string"    (\<open>(\<open>notation=\<open>literal string\<close>\<close>_)\<close>)
 
 ML_file \<open>Tools/string_syntax.ML\<close>