src/Pure/Syntax/mixfix.ML

   ("_idts",        "[idt, idts] => idts",           Mixfix ("_/ _", [1, 0], 0)),
   ("",             "idt => pttrn",                  Delimfix "_"),
   ("",             "pttrn => pttrns",               Delimfix "_"),
   ("_pttrns",      "[pttrn, pttrns] => pttrns",     Mixfix ("_/ _", [1, 0], 0)),
   ("",             "id => aprop",                   Delimfix "_"),
+  ("",             "longid => aprop",               Delimfix "_"),
   ("",             "var => aprop",                  Delimfix "_"),
   ("_aprop",       "aprop => prop",                 Delimfix "PROP _"),
   ("",             "prop => asms",                  Delimfix "_"),
   ("_asms",        "[prop, asms] => asms",          Delimfix "_;/ _"),
   ("_bigimpl",     "[asms, prop] => prop",          Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   ("_ofclass",     "[type, logic] => prop",         Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   ("_mk_ofclass",  "_",                             NoSyn),
   ("_mk_ofclassS", "_",                             NoSyn),
   ("_K",           "_",                             NoSyn),
   ("",             "id => logic",                   Delimfix "_"),
+  ("",             "longid => logic",               Delimfix "_"),
   ("",             "var => logic",                  Delimfix "_")];
 
 val pure_appl_syntax =
  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
   ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))];

   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
 
-end;
+
+end;