src/Pure/Syntax/parser.ML

 val UnknownStart = EndToken;       (*productions for which no starting token is
                                      known yet are associated with this token*)
 
 (* get all NTs that are connected with a list of NTs
    (used for expanding chain list)*)
-fun connected_with _ [] relatives = relatives
+fun connected_with _ ([]: nt_tag list) relatives = relatives
   | connected_with chains (root :: roots) relatives =
     let val branches = subtract (op =) relatives (these (AList.lookup (op =) chains root));
     in connected_with chains (branches @ roots) (branches @ relatives) end;
 
 (* convert productions to grammar;

                                        else (to, new_tks) :: added)
                 end;
 
             val tos = connected_with chains' [lhs] [lhs];
         in (copy_lookahead tos [],
-            (if member (op =) lambdas lhs then tos else []) union lambdas)
+            gen_union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
         end;
 
       (*test if new production can produce lambda
         (rhs must either be empty or only consist of lambda NTs)*)
       val (new_lambda, lambdas') =
         if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
                     | (Terminal _) => false) rhs then
-          (true, lambdas' union (connected_with chains' [lhs] [lhs]))
+          (true, gen_union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
         else
           (false, lambdas');
 
       (*list optional terminal and all nonterminals on which the lookahead
         of a production depends*)

                           ((if is_some tk then [the tk] else []) @
                             Library.foldl token_union ([], map starts_for_nt nts));
 
                         val added_tks' = token_union (new_tks, added_tks);
 
-                        val nt_dependencies' = nts union nt_dependencies;
+                        val nt_dependencies' = gen_union (op =) (nts, nt_dependencies);
 
                         (*associate production with new starting tokens*)
-                        fun copy [] nt_prods = nt_prods
+                        fun copy ([]: token option list) nt_prods = nt_prods
                           | copy (tk :: tks) nt_prods =
                             let val old_prods = these (AList.lookup (op =) nt_prods tk);
 
                                 val prods' = p :: old_prods;
                             in nt_prods

                             if member (op =) tk_prods new_prod then (tk_prods, false)
                             else (new_prod :: tk_prods, true)
                           else (new_prod :: tk_prods, true);
 
                         val prods' = prods
-                                     |> is_new' ? AList.update (op =) (tk, tk_prods');
+                          |> is_new' ? AList.update (op =) (tk: token option, tk_prods');
                     in store tks prods' (is_new orelse is_new') end;
 
                 val (nt_prods', prod_count', changed) =
                   if nt = lhs then store opt_starts nt_prods false
                               else (nt_prods, prod_count, false);

 
                 (*copy productions whose lookahead depends on changed_nt;
                   if key = SOME UnknownToken then tk_prods is used to hold
                   the productions not copied*)
                 fun update_prods [] result = result
-                  | update_prods ((p as (rhs, _, _)) :: ps)
+                  | update_prods ((p as (rhs, _: string, _: nt_tag)) :: ps)
                       (tk_prods, nt_prods) =
                     let
                       (*lookahead dependency for production*)
                       val (tk, depends) = lookahead_dependency lambdas' rhs [];
 

                       val lambda = length depends > 1 orelse
                                    not (null depends) andalso is_some tk
                                    andalso member (op =) new_tks (the tk);
 
                       (*associate production with new starting tokens*)
-                      fun copy [] nt_prods = nt_prods
+                      fun copy ([]: token list) nt_prods = nt_prods
                         | copy (tk :: tks) nt_prods =
                           let
                             val tk_prods = (these o AList.lookup (op =) nt_prods) (SOME tk);
 
                             val tk_prods' =

     fun pretty_nt (name, tag) =
       let
         fun prod_of_chain from_ = ([Nonterminal (from_, ~1)], "", ~1);
 
         val nt_prods =
-          Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @
+          Library.foldl (gen_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;
 
   in maps pretty_nt taglist end;
 

                        prods = Array.array (0, (([], []), []))};
 
 
 (*Invert list of chain productions*)
 fun inverse_chains [] result = result
-  | inverse_chains ((root, branches) :: cs) result =
-    let fun add [] result = result
+  | inverse_chains ((root, branches: nt_tag list) :: cs) result =
+    let fun add ([]: nt_tag list) result = result
           | add (id :: ids) result =
             let val old = (these o AList.lookup (op =) result) id;
             in add ids (AList.update (op =) (id, root :: old) result) end;
     in inverse_chains cs (add branches result) end;
 

 
     (*convert prods2 array to productions*)
     fun process_nt ~1 result = result
       | process_nt nt result =
         let
-          val nt_prods = Library.foldl (op union)
+          val nt_prods = Library.foldl (gen_union op =)
                              ([], map snd (snd (Array.sub (prods2, nt))));
           val lhs_tag = convert_tag nt;
 
           (*convert tags in rhs*)
           fun process_rhs [] result = result

                       val (_, nt_prods) = Array.sub (prods, nt);
 
                       val chained = map (fn nt => (nt, minPrec))
                                         ((these o AList.lookup (op =) chains) nt);
                   in get_starts (chained @ nts)
-                                ((get nt_prods []) union result)
+                                (gen_union (op =) (get nt_prods [], result))
                   end;
 
               val nts =
                 map_filter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
                            SOME (a, prec) | _ => NONE)