thy_syntax.ML
changeset 196 61620d959717
parent 172 8aa51768ade4
child 201 4d0545e93c0d
equal deleted inserted replaced
195:df6b3bd14dcb 196:61620d959717
   137     \end;\n");
   137     \end;\n");
   138 
   138 
   139   (*parsers*)
   139   (*parsers*)
   140   val tvars = type_args >> map (cat "dtVar");
   140   val tvars = type_args >> map (cat "dtVar");
   141   val typ =
   141   val typ =
   142     tvars -- name >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
   142     tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
   143     type_var >> cat "dtVar";
   143     type_var >> cat "dtVar";
   144   val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
   144   val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
   145   val constructor = name -- opt_typs -- opt_mixfix;
   145   val constructor = name -- opt_typs -- opt_mixfix;
   146 in
   146 in
   147   val datatype_decl =
   147   val datatype_decl =