
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -95,12 +95,13 @@
 
 end
 
+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" == fcons
-
+  "_fset_args" "_fset" == fcons
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"




