diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Map.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -61,7 +61,7 @@
   ""         :: "maplet \<Rightarrow> updbind"              (\<open>_\<close>)
   ""         :: "maplet \<Rightarrow> maplets"             (\<open>_\<close>)
   "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>)
-  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(1[_])\<close>)
+  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)
 
 syntax (ASCII)