src/Pure/Syntax/parser.ML

   Gram of
    {nt_count: int,
     prod_count: int,
     tags: nt_tag Symtab.table,
     chains: unit Int_Graph.T,
-    lambdas: nt_tag list,
+    lambdas: Inttab.set,
     prods: nt_gram Vector.vector};
     (*"tags" is used to map NT names (i.e. strings) to tags;
      chain productions are not stored as normal productions
      but instead as an entry in "chains": from -> to;
      lambda productions are stored as normal productions

                 |> Int_Graph.default_node (from, ())
                 |> Int_Graph.default_node (lhs, ())
                 |> Int_Graph.add_edge (from, lhs))
           | _ => (NONE, false, chains |> Int_Graph.default_node (lhs, ())));
 
-        (*propagate new chain in lookahead and lambda lists;
+        (*propagate new chain in lookahead and lambdas;
           added_starts is used later to associate existing
           productions with new starting tokens*)
         val (added_starts, lambdas') =
           if not new_chain then ([], lambdas)
           else

                     end;
 
               val tos = Int_Graph.all_succs chains' [lhs];
             in
               (copy_lookahead tos [],
-                union (op =) (if member (op =) lambdas lhs then tos else []) lambdas)
+                lambdas |> Inttab.defined lambdas lhs ? fold Inttab.insert_set tos)
             end;
 
         (*test if new production can produce lambda
           (rhs must either be empty or only consist of lambda NTs)*)
-        val (new_lambda, lambdas') =
+        val new_lambdas =
           if forall
-            (fn Nonterminal (id, _) => member (op =) lambdas' id
+            (fn Nonterminal (id, _) => Inttab.defined lambdas' id
               | Terminal _ => false) rhs
-          then (true, union (op =) (Int_Graph.all_succs chains' [lhs]) lambdas')
-          else (false, lambdas');
+          then SOME (filter_out (Inttab.defined lambdas') (Int_Graph.all_succs chains' [lhs]))
+          else NONE;
+        val lambdas'' = fold Inttab.insert_set (these new_lambdas) lambdas';
 
         (*list optional terminal and all nonterminals on which the lookahead
           of a production depends*)
         fun lookahead_dependency _ [] nts = (NONE, nts)
           | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts)
           | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts =
-              if member (op =) lambdas nt then
+              if Inttab.defined lambdas nt then
                 lookahead_dependency lambdas symbs (nt :: nts)
               else (NONE, nt :: nts);
 
         (*get all known starting tokens for a nonterminal*)
         fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));

                       | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda
                             nt_dependencies added_tks nt_prods =
                           let val (tk, nts) = lookahead_dependency lambdas rhs [] in
                             if member (op =) nts l then       (*update production's lookahead*)
                               let
-                                val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
+                                val new_lambda =
+                                  is_none tk andalso forall (Inttab.defined lambdas) nts;
 
                                 val new_tks =
                                   (if is_some tk then [the tk] else [])
                                   |> fold (union_token o starts_for_nt) nts
                                   |> subtract (op =) l_starts;

                             val (add_lambda, nt_dependencies, added_tks, nt_prods') =
                               examine_prods tk_prods false [] [] nt_prods;
 
                             val added_nts = subtract (op =) old_nts nt_dependencies;
 
-                            val added_lambdas' =
-                              if add_lambda then nt :: added_lambdas
-                              else added_lambdas;
+                            val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
                             val _ =
                               Array.update
                                 (prods, nt, ((added_nts @ old_nts, old_tks @ added_tks), nt_prods'));
                               (*N.B. that because the tks component
                                 is used to access existing

                             else
                               process_nts nts added_lambdas' ((nt, added_tks) :: added_starts)
                           end;
 
                     val (added_lambdas, added_starts') = process_nts dependent [] added_starts;
-                    val added_lambdas' = subtract (op =) lambdas added_lambdas;
+                    val added_lambdas' = filter_out (Inttab.defined lambdas) added_lambdas;
                   in
-                    propagate_lambda (ls @ added_lambdas') added_starts' (added_lambdas' @ lambdas)
+                    propagate_lambda (ls @ added_lambdas') added_starts'
+                      (fold Inttab.insert_set added_lambdas' lambdas)
                   end;
-          in propagate_lambda (subtract (op =) lambdas lambdas') added_starts lambdas' end;
+          in
+            propagate_lambda
+              (Inttab.fold (fn (l, ()) => not (Inttab.defined lambdas l) ? cons l) lambdas'' [])
+              added_starts lambdas''
+          end;
 
         (*insert production into grammar*)
         val (added_starts', _) =
           if is_some chain
           then (added_starts', prod_count)  (*don't store chain production*)

               val start_tks =
                 (if is_some start_tk then [the start_tk] else [])
                 |> fold (union_token o starts_for_nt) start_nts;
 
               val opt_starts =
-               (if new_lambda then [NONE]
+               (if is_some new_lambdas then [NONE]
                 else if null start_tks then [SOME unknown_start]
                 else []) @ map SOME start_tks;
 
               (*add lhs NT to list of dependent NTs in lookahead*)
               fun add_nts [] = ()

   Gram
    {nt_count = 0,
     prod_count = 0,
     tags = Symtab.empty,
     chains = Int_Graph.empty,
-    lambdas = [],
+    lambdas = Inttab.empty,
     prods = Vector.fromList [(([], []), [])]};
 
 
 (*Add productions to a grammar*)
 fun extend_gram [] gram = gram