src/Pure/Syntax/type_ext.ML
changeset 764 b60e77395d1a
parent 640 b26753b92f98
child 1511 09354d37a5ab
equal deleted inserted replaced
763:d5a626aacdd3 764:b60e77395d1a
   155 
   155 
   156 val sortT = Type ("sort", []);
   156 val sortT = Type ("sort", []);
   157 val classesT = Type ("classes", []);
   157 val classesT = Type ("classes", []);
   158 val typesT = Type ("types", []);
   158 val typesT = Type ("types", []);
   159 
   159 
   160 val type_ext = syn_ext
   160 val type_ext = mk_syn_ext false []
   161   [logic, "type"] [logic, "type"]
       
   162   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   161   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   163    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   162    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   164    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   163    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   165    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   164    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   166    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   165    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   183    [("fun", fun_ast_tr')])
   182    [("fun", fun_ast_tr')])
   184   ([], []);
   183   ([], []);
   185 
   184 
   186 
   185 
   187 end;
   186 end;
   188