diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -95,13 +95,10 @@
 
 end
 
-nonterminal fset_args
 syntax
-  "" :: "'a \<Rightarrow> fset_args"  (\<open>_\<close>)
-  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  (\<open>_,/ _\<close>)
-  "_fset" :: "fset_args => 'a fset"  (\<open>{|(_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
 syntax_consts
-  "_fset_args" "_fset" == fcons
+  fcons
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"