src/HOL/Quotient_Examples/Lift_FSet.thy

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -98,6 +98,9 @@
 syntax
   "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
 
+syntax_consts
+  "_insert_fset" == fcons
+
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"