diff -r 713424d012fd -r 70076ba563d2 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -164,12 +164,13 @@
 lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
   by simp
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == finsert
-
+  "_fset_args" "_fset" == finsert
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"