diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -167,6 +167,9 @@
 syntax
   "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
 
+syntax_consts
+  "_insert_fset" == finsert
+
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
@@ -200,6 +203,10 @@
   "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
   "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_fBall" \<rightleftharpoons> FSet.Ball and
+  "_fBex" \<rightleftharpoons> FSet.Bex
+
 translations
   "\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
   "\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"