src/Pure/pure_thy.ML

     ("",            typ "id_position \<Rightarrow> aprop",        Mixfix.mixfix "_"),
     ("",            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 "(\<open>open_block notation=\<open>mixfix atomic prop\<close>\<close>PROP _)"),
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix 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",
       mixfix ("(\<open>notation=\<open>infix \<Longrightarrow>\<close>\<close>(1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
-    ("_ofclass",    typ "type \<Rightarrow> logic \<Rightarrow> prop",       Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"),
+    ("_ofclass",    typ "type \<Rightarrow> logic \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>indent=1 notation=\<open>mixfix OFCLASS\<close>\<close>OFCLASS/(1'(_,/ _')))"),
     ("_mk_ofclass", typ "dummy",                       NoSyn),
-    ("_TYPE",       typ "type \<Rightarrow> logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
+    ("_TYPE",       typ "type \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>indent=1 notation=\<open>mixfix TYPE\<close>\<close>TYPE/(1'(_')))"),
     ("",            typ "id_position \<Rightarrow> logic",        Mixfix.mixfix "_"),
     ("",            typ "longid_position \<Rightarrow> logic",    Mixfix.mixfix "_"),
     ("",            typ "var_position \<Rightarrow> logic",       Mixfix.mixfix "_"),
     ("_DDDOT",      typ "logic",                       Mixfix.mixfix "\<dots>"),
     ("_strip_positions", typ "'a", NoSyn),

     ("_position",   typ "var \<Rightarrow> var_position",         Mixfix.mixfix "_"),
     ("_position",   typ "str_token \<Rightarrow> str_position",   Mixfix.mixfix "_"),
     ("_position",   typ "string_token \<Rightarrow> string_position", Mixfix.mixfix "_"),
     ("_position",   typ "cartouche \<Rightarrow> cartouche_position", Mixfix.mixfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
-    ("_context_const", typ "id_position \<Rightarrow> logic",     Mixfix.mixfix "CONST _"),
-    ("_context_const", typ "id_position \<Rightarrow> aprop",     Mixfix.mixfix "CONST _"),
-    ("_context_const", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"),
-    ("_context_const", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"),
-    ("_context_xconst", typ "id_position \<Rightarrow> logic",    Mixfix.mixfix "XCONST _"),
-    ("_context_xconst", typ "id_position \<Rightarrow> aprop",    Mixfix.mixfix "XCONST _"),
-    ("_context_xconst", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"),
-    ("_context_xconst", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"),
+    ("_context_const", typ "id_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_const", typ "id_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_const", typ "longid_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_const", typ "longid_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_xconst", typ "id_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
+    ("_context_xconst", typ "id_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
+    ("_context_xconst", typ "longid_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
+    ("_context_xconst", typ "longid_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
     (const "Pure.dummy_pattern", typ "aprop",          Mixfix.mixfix "'_"),
-    ("_sort_constraint", typ "type \<Rightarrow> prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
-    (const "Pure.term", typ "logic \<Rightarrow> prop",           Mixfix.mixfix "TERM _"),
+    ("_sort_constraint", typ "type \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>indent=1 notation=\<open>mixfix SORT_CONSTRAINT\<close>\<close>SORT'_CONSTRAINT/(1'(_')))"),
+    (const "Pure.term", typ "logic \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix TERM\<close>\<close>TERM _)"),
     (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
   #> Sign.syntax_global true Syntax.mode_default applC_syntax
   #> Sign.syntax_global true (Print_Mode.ASCII, true)
    [(tycon "fun",         typ "type \<Rightarrow> type \<Rightarrow> type",
       mixfix ("(\<open>notation=\<open>infix =>\<close>\<close>_/ => _)", [1, 0], 0)),