src/HOL/Set.thy

--- a/src/HOL/Set.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Set.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -144,7 +144,7 @@
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
 syntax
-  "_Finset" :: "args \<Rightarrow> 'a set"    (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
+  "_Finset" :: "args \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 syntax_consts
   insert
 translations