src/Pure/Syntax/type_ext.ML
changeset 7500 299949eddba8
parent 6901 5e20ddfdf3c7
child 8895 2913a54e64cf
equal deleted inserted replaced
7499:23e090051cb8 7500:299949eddba8
   154 val classesT = Type ("classes", []);
   154 val classesT = Type ("classes", []);
   155 val typesT = Type ("types", []);
   155 val typesT = Type ("types", []);
   156 
   156 
   157 local open Lexicon SynExt in
   157 local open Lexicon SynExt in
   158 
   158 
   159 val type_ext = mk_syn_ext false []
   159 val type_ext = mk_syn_ext false ["dummy"]
   160   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   160   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   161    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   161    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   162    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   162    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   163    Mfix ("_",           longidT --> typeT,             "", [], max_pri),
   163    Mfix ("_",           longidT --> typeT,             "", [], max_pri),
   164    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   164    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),