--- a/src/Pure/pure_thy.ML Sun Oct 06 21:55:31 2024 +0200
+++ b/src/Pure/pure_thy.ML Sun Oct 06 22:56:07 2024 +0200
@@ -113,11 +113,14 @@
("_class_name", typ "id \<Rightarrow> class_name", Mixfix.mixfix "_"),
("_class_name", typ "longid \<Rightarrow> class_name", Mixfix.mixfix "_"),
("_dummy_sort", typ "sort", Mixfix.mixfix "'_"),
- ("_topsort", typ "sort", Mixfix.mixfix "{}"),
- ("_sort", typ "classes \<Rightarrow> sort", Mixfix.mixfix "{_}"),
+ ("_topsort", typ "sort",
+ Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix sort\<close>\<close>{})"),
+ ("_sort", typ "classes \<Rightarrow> sort",
+ Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix sort\<close>\<close>{_})"),
("", typ "class_name \<Rightarrow> classes", Mixfix.mixfix "_"),
("_classes", typ "class_name \<Rightarrow> classes \<Rightarrow> classes", Mixfix.mixfix "_,_"),
- ("_tapp", typ "type \<Rightarrow> type_name \<Rightarrow> type", mixfix ("_ _", [1000, 0], 1000)),
+ ("_tapp", typ "type \<Rightarrow> type_name \<Rightarrow> type",
+ mixfix ("(\<open>open_block notation=\<open>type_application\<close>\<close>_ _)", [1000, 0], 1000)),
("_tappl", typ "type \<Rightarrow> types \<Rightarrow> type_name \<Rightarrow> type",
Mixfix.mixfix "(\<open>notation=type_application\<close>(1'(_,/ _')) _)"),
("", typ "type \<Rightarrow> types", Mixfix.mixfix "_"),
@@ -149,7 +152,8 @@
("", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "_"),
("", typ "var_position \<Rightarrow> aprop", Mixfix.mixfix "_"),
("_DDDOT", typ "aprop", Mixfix.mixfix "\<dots>"),
- ("_aprop", typ "aprop \<Rightarrow> prop", Mixfix.mixfix "PROP _"),
+ ("_aprop", typ "aprop \<Rightarrow> prop",
+ Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix atomic prop\<close>\<close>PROP _)"),
("_asm", typ "prop \<Rightarrow> asms", Mixfix.mixfix "_"),
("_asms", typ "prop \<Rightarrow> asms \<Rightarrow> asms", Mixfix.mixfix "_;/ _"),
("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop",