diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -117,7 +117,7 @@
 We shall prove that this notion is unique up to order isomorphism, meaning
 that order isomorphism shall be the true identity of cardinals.\<close>
 
-definition card_of :: "'a set \<Rightarrow> 'a rel" (\<open>|_|\<close> )
+definition card_of :: "'a set \<Rightarrow> 'a rel" (\<open>(\<open>open_block notation=\<open>mixfix card_of\<close>\<close>|_|)\<close>)
   where "card_of A = (SOME r. card_order_on A r)"
 
 lemma card_of_card_order_on: "card_order_on A |A|"