diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Cardinal.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -25,8 +25,8 @@
     "A \<prec> B \<equiv> A \<lesssim> B \<and> \<not>(A \<approx> B)"
 
 definition
-  cardinal :: "i\<Rightarrow>i"           (\<open>|_|\<close>)  where
-    "|A| \<equiv> (\<mu> i. i \<approx> A)"
+  cardinal :: "i\<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>mixfix cardinal\<close>\<close>|_|)\<close>)
+  where "|A| \<equiv> (\<mu> i. i \<approx> A)"
 
 definition
   Finite   :: "i\<Rightarrow>o"  where