src/Pure/Syntax/parser.ML

--- a/src/Pure/Syntax/parser.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -101,7 +101,7 @@
 
             val tos = connected_with chains' [lhs] [lhs];
         in (copy_lookahead tos [],
-            gen_union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
+            union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
         end;
 
       (*test if new production can produce lambda
@@ -109,7 +109,7 @@
       val (new_lambda, lambdas') =
         if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
                     | (Terminal _) => false) rhs then
-          (true, gen_union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
+          (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
         else
           (false, lambdas');
 
@@ -125,7 +125,7 @@
       (*get all known starting tokens for a nonterminal*)
       fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
 
-      val token_union = gen_union matching_tokens;
+      val token_union = union matching_tokens;
 
       (*update prods, lookaheads, and lambdas according to new lambda NTs*)
       val (added_starts', lambdas') =
@@ -147,7 +147,7 @@
                     in
                       if member (op =) nts l then       (*update production's lookahead*)
                       let
-                        val new_lambda = is_none tk andalso gen_subset (op =) (nts, lambdas);
+                        val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
 
                         val new_tks = subtract (op =) l_starts
                           ((if is_some tk then [the tk] else []) @
@@ -155,7 +155,7 @@
 
                         val added_tks' = token_union (new_tks, added_tks);
 
-                        val nt_dependencies' = gen_union (op =) (nts, nt_dependencies);
+                        val nt_dependencies' = union (op =) (nts, nt_dependencies);
 
                         (*associate production with new starting tokens*)
                         fun copy ([]: token option list) nt_prods = nt_prods
@@ -413,7 +413,7 @@
         fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
 
         val nt_prods =
-          Library.foldl (gen_union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
+          Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
           map prod_of_chain ((these o AList.lookup (op =) chains) tag);
       in map (pretty_prod name) nt_prods end;
 
@@ -562,7 +562,7 @@
     fun process_nt ~1 result = result
       | process_nt nt result =
         let
-          val nt_prods = Library.foldl (gen_union op =)
+          val nt_prods = Library.foldl (union op =)
                              ([], map snd (snd (Array.sub (prods2, nt))));
           val lhs_tag = convert_tag nt;