src/Pure/Syntax/mixfix.ML

   ("",             "pttrn => pttrns",               Delimfix "_"),
   ("_pttrns",      "[pttrn, pttrns] => pttrns",     Mixfix ("_/ _", [1, 0], 0)),
   ("",             "id => aprop",                   Delimfix "_"),
   ("",             "longid => aprop",               Delimfix "_"),
   ("",             "var => aprop",                  Delimfix "_"),
-  ("_BIND",        "id => aprop",                   Delimfix "??_"),
   ("_DDDOT",       "aprop",                         Delimfix "..."),
   ("_aprop",       "aprop => prop",                 Delimfix "PROP _"),
   ("",             "prop => asms",                  Delimfix "_"),
   ("_asms",        "[prop, asms] => asms",          Delimfix "_;/ _"),
   ("_bigimpl",     "[asms, prop] => prop",          Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),

   ("_TYPE",        "type => logic",                 Delimfix "(1TYPE/(1'(_')))"),
   ("_K",           "_",                             NoSyn),
   ("",             "id => logic",                   Delimfix "_"),
   ("",             "longid => logic",               Delimfix "_"),
   ("",             "var => logic",                  Delimfix "_"),
-  ("_BIND",        "id => logic",                   Delimfix "??_"),
   ("_DDDOT",       "logic",                         Delimfix "...")];
 
 val pure_appl_syntax =
  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),
   ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri))];