clarified simple mixfix;
authorwenzelm
Wed Mar 30 15:15:12 2016 +0200 (2016-03-30)
changeset 627615c672b22dcc2
parent 62760 aabcc727aa2d
child 62762 ac039c4981b6
clarified simple mixfix;
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/mixfix.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Mar 30 14:59:12 2016 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Mar 30 15:15:12 2016 +0200
     1.3 @@ -1960,7 +1960,7 @@
     1.4      val setT = HOLogic.mk_setT T
     1.5      val elems = HOLogic.mk_set T ts
     1.6      val ([dots], ctxt') = ctxt
     1.7 -      |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Delimfix (\<open>...\<close>, Position.no_range))]
     1.8 +      |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix.mixfix "...")]
     1.9      (* check expected values *)
    1.10      val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
    1.11      val () =
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Wed Mar 30 14:59:12 2016 +0200
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Wed Mar 30 15:15:12 2016 +0200
     2.3 @@ -42,7 +42,6 @@
     2.4  (** constants for application and abstraction **)
     2.5  
     2.6  fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
     2.7 -fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
     2.8  
     2.9  fun add_proof_syntax thy =
    2.10    thy
    2.11 @@ -58,7 +57,7 @@
    2.12       ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
    2.13       ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
    2.14       ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
    2.15 -     ((Binding.make ("MinProof", @{here}), proofT), delimfix "?")]
    2.16 +     ((Binding.make ("MinProof", @{here}), proofT), Mixfix.mixfix "?")]
    2.17    |> Sign.add_nonterminals_global
    2.18      [Binding.make ("param", @{here}),
    2.19       Binding.make ("params", @{here})]
    2.20 @@ -67,9 +66,9 @@
    2.21       ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
    2.22       ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
    2.23       ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
    2.24 -     ("", paramT --> paramT, delimfix "'(_')"),
    2.25 -     ("", idtT --> paramsT, delimfix "_"),
    2.26 -     ("", paramT --> paramsT, delimfix "_")]
    2.27 +     ("", paramT --> paramT, Mixfix.mixfix "'(_')"),
    2.28 +     ("", idtT --> paramsT, Mixfix.mixfix "_"),
    2.29 +     ("", paramT --> paramsT, Mixfix.mixfix "_")]
    2.30    |> Sign.add_syntax (Print_Mode.ASCII, true)
    2.31      [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
    2.32       (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:59:12 2016 +0200
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 15:15:12 2016 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4    datatype mixfix =
     3.5      NoSyn |
     3.6      Mixfix of Input.source * int list * int * Position.range |
     3.7 -    Delimfix of Input.source * Position.range |
     3.8      Infix of Input.source * int * Position.range |
     3.9      Infixl of Input.source * int * Position.range |
    3.10      Infixr of Input.source * int * Position.range |
    3.11 @@ -20,6 +19,7 @@
    3.12  signature MIXFIX =
    3.13  sig
    3.14    include BASIC_MIXFIX
    3.15 +  val mixfix: string -> mixfix
    3.16    val is_empty: mixfix -> bool
    3.17    val equal: mixfix * mixfix -> bool
    3.18    val range_of: mixfix -> Position.range
    3.19 @@ -42,20 +42,20 @@
    3.20  datatype mixfix =
    3.21    NoSyn |
    3.22    Mixfix of Input.source * int list * int * Position.range |
    3.23 -  Delimfix of Input.source * Position.range |
    3.24    Infix of Input.source * int * Position.range |
    3.25    Infixl of Input.source * int * Position.range |
    3.26    Infixr of Input.source * int * Position.range |
    3.27    Binder of Input.source * int * int * Position.range |
    3.28    Structure of Position.range;
    3.29  
    3.30 +fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range);
    3.31 +
    3.32  fun is_empty NoSyn = true
    3.33    | is_empty _ = false;
    3.34  
    3.35  fun equal (NoSyn, NoSyn) = true
    3.36    | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
    3.37        Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'
    3.38 -  | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy')
    3.39    | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
    3.40    | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
    3.41    | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
    3.42 @@ -66,7 +66,6 @@
    3.43  
    3.44  fun range_of NoSyn = Position.no_range
    3.45    | range_of (Mixfix (_, _, _, range)) = range
    3.46 -  | range_of (Delimfix (_, range)) = range
    3.47    | range_of (Infix (_, _, range)) = range
    3.48    | range_of (Infixl (_, _, range)) = range
    3.49    | range_of (Infixr (_, _, range)) = range
    3.50 @@ -77,7 +76,6 @@
    3.51  
    3.52  fun reset_pos NoSyn = NoSyn
    3.53    | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
    3.54 -  | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range)
    3.55    | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range)
    3.56    | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range)
    3.57    | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range)
    3.58 @@ -100,7 +98,6 @@
    3.59  fun pretty_mixfix NoSyn = Pretty.str ""
    3.60    | pretty_mixfix (Mixfix (s, ps, p, _)) =
    3.61        parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
    3.62 -  | pretty_mixfix (Delimfix (s, _)) = parens [quoted s]
    3.63    | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    3.64    | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    3.65    | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    3.66 @@ -115,7 +112,6 @@
    3.67  
    3.68  fun mixfix_args NoSyn = 0
    3.69    | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy
    3.70 -  | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy
    3.71    | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
    3.72    | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
    3.73    | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
    3.74 @@ -141,8 +137,6 @@
    3.75      fun mfix_of (_, _, NoSyn) = NONE
    3.76        | mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
    3.77            SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
    3.78 -      | mfix_of (t, ty, Delimfix (sy, range)) =
    3.79 -          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, Position.set_range range))
    3.80        | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
    3.81        | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
    3.82        | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
    3.83 @@ -183,8 +177,6 @@
    3.84      fun mfix_of (_, _, NoSyn) = []
    3.85        | mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
    3.86            [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
    3.87 -      | mfix_of (c, ty, Delimfix (sy, range)) =
    3.88 -          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, Position.set_range range)]
    3.89        | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
    3.90        | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
    3.91        | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range
     4.1 --- a/src/Pure/pure_thy.ML	Wed Mar 30 14:59:12 2016 +0200
     4.2 +++ b/src/Pure/pure_thy.ML	Wed Mar 30 15:15:12 2016 +0200
     4.3 @@ -23,7 +23,6 @@
     4.4  val qualify = Binding.qualify true Context.PureN;
     4.5  
     4.6  fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
     4.7 -fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
     4.8  fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range);
     4.9  fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
    4.10  fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
    4.11 @@ -36,7 +35,7 @@
    4.12    ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
    4.13  
    4.14  val applC_syntax =
    4.15 - [("",       typ "'a => cargs",                  delimfix "_"),
    4.16 + [("",       typ "'a => cargs",                  Mixfix.mixfix "_"),
    4.17    ("_cargs", typ "'a => cargs => cargs",         mixfix ("_/ _", [1000, 1000], 1000)),
    4.18    ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
    4.19    ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
    4.20 @@ -87,99 +86,99 @@
    4.21          "class_name"]))
    4.22    #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
    4.23    #> Sign.add_syntax Syntax.mode_default
    4.24 -   [("",            typ "prop' => prop",               delimfix "_"),
    4.25 -    ("",            typ "logic => any",                delimfix "_"),
    4.26 -    ("",            typ "prop' => any",                delimfix "_"),
    4.27 -    ("",            typ "logic => logic",              delimfix "'(_')"),
    4.28 -    ("",            typ "prop' => prop'",              delimfix "'(_')"),
    4.29 +   [("",            typ "prop' => prop",               Mixfix.mixfix "_"),
    4.30 +    ("",            typ "logic => any",                Mixfix.mixfix "_"),
    4.31 +    ("",            typ "prop' => any",                Mixfix.mixfix "_"),
    4.32 +    ("",            typ "logic => logic",              Mixfix.mixfix "'(_')"),
    4.33 +    ("",            typ "prop' => prop'",              Mixfix.mixfix "'(_')"),
    4.34      ("_constrain",  typ "logic => type => logic",      mixfix ("_::_", [4, 0], 3)),
    4.35      ("_constrain",  typ "prop' => type => prop'",      mixfix ("_::_", [4, 0], 3)),
    4.36      ("_ignore_type", typ "'a",                         NoSyn),
    4.37 -    ("",            typ "tid_position => type",        delimfix "_"),
    4.38 -    ("",            typ "tvar_position => type",       delimfix "_"),
    4.39 -    ("",            typ "type_name => type",           delimfix "_"),
    4.40 -    ("_type_name",  typ "id => type_name",             delimfix "_"),
    4.41 -    ("_type_name",  typ "longid => type_name",         delimfix "_"),
    4.42 +    ("",            typ "tid_position => type",        Mixfix.mixfix "_"),
    4.43 +    ("",            typ "tvar_position => type",       Mixfix.mixfix "_"),
    4.44 +    ("",            typ "type_name => type",           Mixfix.mixfix "_"),
    4.45 +    ("_type_name",  typ "id => type_name",             Mixfix.mixfix "_"),
    4.46 +    ("_type_name",  typ "longid => type_name",         Mixfix.mixfix "_"),
    4.47      ("_ofsort",     typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
    4.48      ("_ofsort",     typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
    4.49      ("_dummy_ofsort", typ "sort => type",              mixfix ("'_()::_", [0], 1000)),
    4.50 -    ("",            typ "class_name => sort",          delimfix "_"),
    4.51 -    ("_class_name", typ "id => class_name",            delimfix "_"),
    4.52 -    ("_class_name", typ "longid => class_name",        delimfix "_"),
    4.53 -    ("_topsort",    typ "sort",                        delimfix "{}"),
    4.54 -    ("_sort",       typ "classes => sort",             delimfix "{_}"),
    4.55 -    ("",            typ "class_name => classes",       delimfix "_"),
    4.56 -    ("_classes",    typ "class_name => classes => classes", delimfix "_,_"),
    4.57 +    ("",            typ "class_name => sort",          Mixfix.mixfix "_"),
    4.58 +    ("_class_name", typ "id => class_name",            Mixfix.mixfix "_"),
    4.59 +    ("_class_name", typ "longid => class_name",        Mixfix.mixfix "_"),
    4.60 +    ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
    4.61 +    ("_sort",       typ "classes => sort",             Mixfix.mixfix "{_}"),
    4.62 +    ("",            typ "class_name => classes",       Mixfix.mixfix "_"),
    4.63 +    ("_classes",    typ "class_name => classes => classes", Mixfix.mixfix "_,_"),
    4.64      ("_tapp",       typ "type => type_name => type",   mixfix ("_ _", [1000, 0], 1000)),
    4.65 -    ("_tappl",      typ "type => types => type_name => type", delimfix "((1'(_,/ _')) _)"),
    4.66 -    ("",            typ "type => types",               delimfix "_"),
    4.67 -    ("_types",      typ "type => types => types",      delimfix "_,/ _"),
    4.68 +    ("_tappl",      typ "type => types => type_name => type", Mixfix.mixfix "((1'(_,/ _')) _)"),
    4.69 +    ("",            typ "type => types",               Mixfix.mixfix "_"),
    4.70 +    ("_types",      typ "type => types => types",      Mixfix.mixfix "_,/ _"),
    4.71      ("\<^type>fun", typ "type => type => type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
    4.72      ("_bracket",    typ "types => type => type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
    4.73 -    ("",            typ "type => type",                delimfix "'(_')"),
    4.74 -    ("\<^type>dummy", typ "type",                      delimfix "'_"),
    4.75 +    ("",            typ "type => type",                Mixfix.mixfix "'(_')"),
    4.76 +    ("\<^type>dummy", typ "type",                      Mixfix.mixfix "'_"),
    4.77      ("_type_prop",  typ "'a",                          NoSyn),
    4.78      ("_lambda",     typ "pttrns => 'a => logic",       mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
    4.79      ("_abs",        typ "'a",                          NoSyn),
    4.80 -    ("",            typ "'a => args",                  delimfix "_"),
    4.81 -    ("_args",       typ "'a => args => args",          delimfix "_,/ _"),
    4.82 -    ("",            typ "id_position => idt",          delimfix "_"),
    4.83 -    ("_idtdummy",   typ "idt",                         delimfix "'_"),
    4.84 +    ("",            typ "'a => args",                  Mixfix.mixfix "_"),
    4.85 +    ("_args",       typ "'a => args => args",          Mixfix.mixfix "_,/ _"),
    4.86 +    ("",            typ "id_position => idt",          Mixfix.mixfix "_"),
    4.87 +    ("_idtdummy",   typ "idt",                         Mixfix.mixfix "'_"),
    4.88      ("_idtyp",      typ "id_position => type => idt",  mixfix ("_::_", [], 0)),
    4.89      ("_idtypdummy", typ "type => idt",                 mixfix ("'_()::_", [], 0)),
    4.90 -    ("",            typ "idt => idt",                  delimfix "'(_')"),
    4.91 -    ("",            typ "idt => idts",                 delimfix "_"),
    4.92 +    ("",            typ "idt => idt",                  Mixfix.mixfix "'(_')"),
    4.93 +    ("",            typ "idt => idts",                 Mixfix.mixfix "_"),
    4.94      ("_idts",       typ "idt => idts => idts",         mixfix ("_/ _", [1, 0], 0)),
    4.95 -    ("",            typ "idt => pttrn",                delimfix "_"),
    4.96 -    ("",            typ "pttrn => pttrns",             delimfix "_"),
    4.97 +    ("",            typ "idt => pttrn",                Mixfix.mixfix "_"),
    4.98 +    ("",            typ "pttrn => pttrns",             Mixfix.mixfix "_"),
    4.99      ("_pttrns",     typ "pttrn => pttrns => pttrns",   mixfix ("_/ _", [1, 0], 0)),
   4.100 -    ("",            typ "aprop => aprop",              delimfix "'(_')"),
   4.101 -    ("",            typ "id_position => aprop",        delimfix "_"),
   4.102 -    ("",            typ "longid_position => aprop",    delimfix "_"),
   4.103 -    ("",            typ "var_position => aprop",       delimfix "_"),
   4.104 -    ("_DDDOT",      typ "aprop",                       delimfix "\<dots>"),
   4.105 -    ("_aprop",      typ "aprop => prop",               delimfix "PROP _"),
   4.106 -    ("_asm",        typ "prop => asms",                delimfix "_"),
   4.107 -    ("_asms",       typ "prop => asms => asms",        delimfix "_;/ _"),
   4.108 +    ("",            typ "aprop => aprop",              Mixfix.mixfix "'(_')"),
   4.109 +    ("",            typ "id_position => aprop",        Mixfix.mixfix "_"),
   4.110 +    ("",            typ "longid_position => aprop",    Mixfix.mixfix "_"),
   4.111 +    ("",            typ "var_position => aprop",       Mixfix.mixfix "_"),
   4.112 +    ("_DDDOT",      typ "aprop",                       Mixfix.mixfix "\<dots>"),
   4.113 +    ("_aprop",      typ "aprop => prop",               Mixfix.mixfix "PROP _"),
   4.114 +    ("_asm",        typ "prop => asms",                Mixfix.mixfix "_"),
   4.115 +    ("_asms",       typ "prop => asms => asms",        Mixfix.mixfix "_;/ _"),
   4.116      ("_bigimpl",    typ "asms => prop => prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
   4.117 -    ("_ofclass",    typ "type => logic => prop",       delimfix "(1OFCLASS/(1'(_,/ _')))"),
   4.118 +    ("_ofclass",    typ "type => logic => prop",       Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"),
   4.119      ("_mk_ofclass", typ "dummy",                       NoSyn),
   4.120 -    ("_TYPE",       typ "type => logic",               delimfix "(1TYPE/(1'(_')))"),
   4.121 -    ("",            typ "id_position => logic",        delimfix "_"),
   4.122 -    ("",            typ "longid_position => logic",    delimfix "_"),
   4.123 -    ("",            typ "var_position => logic",       delimfix "_"),
   4.124 -    ("_DDDOT",      typ "logic",                       delimfix "\<dots>"),
   4.125 +    ("_TYPE",       typ "type => logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
   4.126 +    ("",            typ "id_position => logic",        Mixfix.mixfix "_"),
   4.127 +    ("",            typ "longid_position => logic",    Mixfix.mixfix "_"),
   4.128 +    ("",            typ "var_position => logic",       Mixfix.mixfix "_"),
   4.129 +    ("_DDDOT",      typ "logic",                       Mixfix.mixfix "\<dots>"),
   4.130      ("_strip_positions", typ "'a", NoSyn),
   4.131 -    ("_position",   typ "num_token => num_position",   delimfix "_"),
   4.132 -    ("_position",   typ "float_token => float_position", delimfix "_"),
   4.133 -    ("_constify",   typ "num_position => num_const",   delimfix "_"),
   4.134 -    ("_constify",   typ "float_position => float_const", delimfix "_"),
   4.135 -    ("_index",      typ "logic => index",              delimfix "(00\<^bsub>_\<^esub>)"),
   4.136 -    ("_indexdefault", typ "index",                     delimfix ""),
   4.137 -    ("_indexvar",   typ "index",                       delimfix "'\<index>"),
   4.138 +    ("_position",   typ "num_token => num_position",   Mixfix.mixfix "_"),
   4.139 +    ("_position",   typ "float_token => float_position", Mixfix.mixfix "_"),
   4.140 +    ("_constify",   typ "num_position => num_const",   Mixfix.mixfix "_"),
   4.141 +    ("_constify",   typ "float_position => float_const", Mixfix.mixfix "_"),
   4.142 +    ("_index",      typ "logic => index",              Mixfix.mixfix "(00\<^bsub>_\<^esub>)"),
   4.143 +    ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
   4.144 +    ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
   4.145      ("_struct",     typ "index => logic",              NoSyn),
   4.146      ("_update_name", typ "idt",                        NoSyn),
   4.147      ("_constrainAbs", typ "'a",                        NoSyn),
   4.148 -    ("_position_sort", typ "tid => tid_position",      delimfix "_"),
   4.149 -    ("_position_sort", typ "tvar => tvar_position",    delimfix "_"),
   4.150 -    ("_position",   typ "id => id_position",           delimfix "_"),
   4.151 -    ("_position",   typ "longid => longid_position",   delimfix "_"),
   4.152 -    ("_position",   typ "var => var_position",         delimfix "_"),
   4.153 -    ("_position",   typ "str_token => str_position",   delimfix "_"),
   4.154 -    ("_position",   typ "string_token => string_position", delimfix "_"),
   4.155 -    ("_position",   typ "cartouche => cartouche_position", delimfix "_"),
   4.156 +    ("_position_sort", typ "tid => tid_position",      Mixfix.mixfix "_"),
   4.157 +    ("_position_sort", typ "tvar => tvar_position",    Mixfix.mixfix "_"),
   4.158 +    ("_position",   typ "id => id_position",           Mixfix.mixfix "_"),
   4.159 +    ("_position",   typ "longid => longid_position",   Mixfix.mixfix "_"),
   4.160 +    ("_position",   typ "var => var_position",         Mixfix.mixfix "_"),
   4.161 +    ("_position",   typ "str_token => str_position",   Mixfix.mixfix "_"),
   4.162 +    ("_position",   typ "string_token => string_position", Mixfix.mixfix "_"),
   4.163 +    ("_position",   typ "cartouche => cartouche_position", Mixfix.mixfix "_"),
   4.164      ("_type_constraint_", typ "'a",                    NoSyn),
   4.165 -    ("_context_const", typ "id_position => logic",     delimfix "CONST _"),
   4.166 -    ("_context_const", typ "id_position => aprop",     delimfix "CONST _"),
   4.167 -    ("_context_const", typ "longid_position => logic", delimfix "CONST _"),
   4.168 -    ("_context_const", typ "longid_position => aprop", delimfix "CONST _"),
   4.169 -    ("_context_xconst", typ "id_position => logic",    delimfix "XCONST _"),
   4.170 -    ("_context_xconst", typ "id_position => aprop",    delimfix "XCONST _"),
   4.171 -    ("_context_xconst", typ "longid_position => logic", delimfix "XCONST _"),
   4.172 -    ("_context_xconst", typ "longid_position => aprop", delimfix "XCONST _"),
   4.173 -    (const "Pure.dummy_pattern", typ "aprop",          delimfix "'_"),
   4.174 -    ("_sort_constraint", typ "type => prop",           delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   4.175 -    (const "Pure.term", typ "logic => prop",           delimfix "TERM _"),
   4.176 +    ("_context_const", typ "id_position => logic",     Mixfix.mixfix "CONST _"),
   4.177 +    ("_context_const", typ "id_position => aprop",     Mixfix.mixfix "CONST _"),
   4.178 +    ("_context_const", typ "longid_position => logic", Mixfix.mixfix "CONST _"),
   4.179 +    ("_context_const", typ "longid_position => aprop", Mixfix.mixfix "CONST _"),
   4.180 +    ("_context_xconst", typ "id_position => logic",    Mixfix.mixfix "XCONST _"),
   4.181 +    ("_context_xconst", typ "id_position => aprop",    Mixfix.mixfix "XCONST _"),
   4.182 +    ("_context_xconst", typ "longid_position => logic", Mixfix.mixfix "XCONST _"),
   4.183 +    ("_context_xconst", typ "longid_position => aprop", Mixfix.mixfix "XCONST _"),
   4.184 +    (const "Pure.dummy_pattern", typ "aprop",          Mixfix.mixfix "'_"),
   4.185 +    ("_sort_constraint", typ "type => prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   4.186 +    (const "Pure.term", typ "logic => prop",           Mixfix.mixfix "TERM _"),
   4.187      (const "Pure.conjunction", typ "prop => prop => prop", infixr_ ("&&&", 2))]
   4.188    #> Sign.add_syntax Syntax.mode_default applC_syntax
   4.189    #> Sign.add_syntax (Print_Mode.ASCII, true)
   4.190 @@ -189,9 +188,9 @@
   4.191      (const "Pure.eq",     typ "'a => 'a => prop",       infix_ ("==", 2)),
   4.192      (const "Pure.all_binder", typ "idts => prop => prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
   4.193      (const "Pure.imp",    typ "prop => prop => prop",   infixr_ ("==>", 1)),
   4.194 -    ("_DDDOT",            typ "aprop",                  delimfix "..."),
   4.195 +    ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),
   4.196      ("_bigimpl",          typ "asms => prop => prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   4.197 -    ("_DDDOT",            typ "logic",                  delimfix "...")]
   4.198 +    ("_DDDOT",            typ "logic",                  Mixfix.mixfix "...")]
   4.199    #> Sign.add_syntax ("", false)
   4.200     [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
   4.201    #> Sign.add_consts
   4.202 @@ -200,7 +199,7 @@
   4.203      (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
   4.204      (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
   4.205      (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
   4.206 -    (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", delimfix "'_")]
   4.207 +    (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Mixfix.mixfix "'_")]
   4.208    #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
   4.209    #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
   4.210    #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []