src/Pure/Isar/outer_parse.ML
changeset 7352 d98001b492b3
parent 7171 2a245a80a2c5
child 7418 87c12d352bab
equal deleted inserted replaced
7351:1e485129fbc1 7352:d98001b492b3
   171 
   171 
   172 val sort =
   172 val sort =
   173   xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
   173   xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
   174 
   174 
   175 fun gen_arity cod =
   175 fun gen_arity cod =
   176   Scan.optional ($$$ "(" |-- !!! (Scan.repeat1 sort --| $$$ ")")) [] -- cod;
   176   Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
   177 
   177 
   178 val arity = gen_arity sort;
   178 val arity = gen_arity sort;
   179 val simple_arity = gen_arity name;
   179 val simple_arity = gen_arity name;
   180 
   180 
   181 
   181