diff -r 8042869c2072 -r 843dba3d307a src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -133,7 +133,7 @@
 syntax
   "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
   "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
-  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
+  "_Finset" :: "is \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 syntax_consts
   cons
 translations
@@ -196,7 +196,7 @@
 syntax
   "" :: "i \<Rightarrow> tuple_args"  (\<open>_\<close>)
   "_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args"  (\<open>_,/ _\<close>)
-  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(\<open>notation=\<open>mixfix tuple enumeration\<close>\<close>_,/ _)\<rangle>\<close>)
+  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix tuple enumeration\<close>\<close>\<langle>_,/ _\<rangle>)\<close>)
 syntax_consts
   Pair
 translations