src/Pure/Syntax/parser.ML

      chain productions are not stored as normal productions
      but instead as an entry in "chains": from -> to;
      lambda productions are stored as normal productions
      and also as an entry in "lambdas"*)
 
-val union_token = union Lexicon.matching_tokens;
-val subtract_token = subtract Lexicon.matching_tokens;
+fun tokens_match toks =
+  (case apply2 Lexicon.kind_of_token toks of
+    (Lexicon.Literal, Lexicon.Literal) => op = (apply2 Lexicon.str_of_token toks)
+  | kinds => op = kinds);
+
+val tokens_union = union tokens_match;
+val tokens_subtract = subtract tokens_match;
 
 (*productions for which no starting token is
   known yet are associated with this token*)
 val unknown_start = Lexicon.eof;
 

                                 val new_lambda =
                                   is_none tk andalso forall (lambdas_member lambdas) nts;
 
                                 val new_tks =
                                   (if is_some tk then [the tk] else [])
-                                  |> fold (union_token o starts_for_nt) nts
+                                  |> fold (tokens_union o starts_for_nt) nts
                                   |> subtract (op =) l_starts;
 
-                                val added_tks' = union_token added_tks new_tks;
+                                val added_tks' = tokens_union added_tks new_tks;
 
                                 val nt_dependencies' = union (op =) nts nt_dependencies;
 
                                 (*associate production with new starting tokens*)
                                 fun copy ([]: Lexicon.token option list) nt_prods = nt_prods

                 NTs lookahead depends*)
               val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
 
               val start_tks =
                 (if is_some start_tk then [the start_tk] else [])
-                |> fold (union_token o starts_for_nt) start_nts;
+                |> fold (tokens_union o starts_for_nt) start_nts;
 
               val opt_starts =
                (if is_some new_lambdas then [NONE]
                 else if null start_tks then [SOME unknown_start]
                 else []) @ map SOME start_tks;

               fun add_tks [] added prod_count = (added, prod_count)
                 | add_tks (nt :: nts) added prod_count =
                     let
                       val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
 
-                      val new_tks = subtract_token old_tks start_tks;
+                      val new_tks = tokens_subtract old_tks start_tks;
 
                       (*store new production*)
                       fun store [] prods is_new =
                             (prods,
                               if is_some prod_count andalso is_new then

                             val nt_prods'' =
                               if key = SOME unknown_start then
                                 AList.update (op =) (key, tk_prods') nt_prods'
                               else nt_prods';
 
-                            val added_tks = subtract_token old_tks new_tks;
+                            val added_tks = tokens_subtract old_tks new_tks;
                           in
                             if null added_tks then
                               (Array.update (prods, nt, (lookahead, nt_prods''));
                                 process_nts nts added)
                             else

   let
     fun token_assoc (list, key) =
       let
         fun assoc [] result = result
           | assoc ((keyi, pi) :: pairs) result =
-              if is_some keyi andalso Lexicon.matching_tokens (the keyi, key)
+              if is_some keyi andalso tokens_match (the keyi, key)
                  orelse include_none andalso is_none keyi then
                 assoc pairs (pi @ result)
               else assoc pairs result;
       in assoc list [] end;
 

               in
                 processS used' (new_states @ States) (S :: Si, Sii)
               end
           | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
               processS used States
-                (S :: Si,
-                  if Lexicon.matching_tokens (a, c) then movedot_term c S :: Sii else Sii)
+                (S :: Si, if tokens_match (a, c) then movedot_term c S :: Sii else Sii)
           | (A, prec, ts, [], id, j) => (*completer operation*)
               let val tt = if id = "" then ts else [Node (id, rev ts)] in
                 if j = i then (*lambda production?*)
                   let
                     val (prec', used') = update_trees (A, (tt, prec)) used;