src/HOL/Nominal/Examples/Pattern.thy

--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -5,7 +5,7 @@
 begin
 
 no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix map\<close>\<close>[_])\<close>)
 
 atom_decl name