src/Pure/Isar/args.ML
changeset 28941 128459bd72d2
parent 28078 0c420e7579a6
child 28965 1de908189869
equal deleted inserted replaced
28940:df0cb410be35 28941:128459bd72d2
   169 
   169 
   170 val name_source = named >> T.source_of;
   170 val name_source = named >> T.source_of;
   171 val name_source_position = named >> T.source_position_of;
   171 val name_source_position = named >> T.source_position_of;
   172 
   172 
   173 val name = named >> T.content_of;
   173 val name = named >> T.content_of;
   174 val binding = P.position name >> Name.binding_pos;
   174 val binding = P.position name >> Binding.binding_pos;
   175 val alt_name = alt_string >> T.content_of;
   175 val alt_name = alt_string >> T.content_of;
   176 val symbol = symbolic >> T.content_of;
   176 val symbol = symbolic >> T.content_of;
   177 val liberal_name = symbol || name;
   177 val liberal_name = symbol || name;
   178 
   178 
   179 val var = (ident >> T.content_of) :|-- (fn x =>
   179 val var = (ident >> T.content_of) :|-- (fn x =>