src/Pure/Isar/args.ML
changeset 30240 5b25fee0362c
parent 29606 fedb8be05f24
child 30473 e0b66c11e7e4
equal deleted inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c
   168 
   168 
   169 val name_source = named >> T.source_of;
   169 val name_source = named >> T.source_of;
   170 val name_source_position = named >> T.source_position_of;
   170 val name_source_position = named >> T.source_position_of;
   171 
   171 
   172 val name = named >> T.content_of;
   172 val name = named >> T.content_of;
   173 val binding = P.position name >> Binding.name_pos;
   173 val binding = P.position name >> Binding.make;
   174 val alt_name = alt_string >> T.content_of;
   174 val alt_name = alt_string >> T.content_of;
   175 val symbol = symbolic >> T.content_of;
   175 val symbol = symbolic >> T.content_of;
   176 val liberal_name = symbol || name;
   176 val liberal_name = symbol || name;
   177 
   177 
   178 val var = (ident >> T.content_of) :|-- (fn x =>
   178 val var = (ident >> T.content_of) :|-- (fn x =>