--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 30 23:32:26 2024 +0200
@@ -289,7 +289,7 @@
is "Cons" by auto
syntax
- "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
+ "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
syntax_consts
insert_fset
translations