src/Pure/Syntax/parser.ML

         val nt_prods =
           Library.foldl (op union) ([], 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 List.concat (map pretty_nt taglist) end;
+  in maps pretty_nt taglist end;
 
 
 (** Operations on gramars **)
 
 (*The mother of all grammars*)

                   in get_starts (chained @ nts)
                                 ((get nt_prods []) union result)
                   end;
 
               val nts =
-                List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
+                map_filter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
                            SOME (a, prec) | _ => NONE)
                           (Array.sub (stateset, i-1));
               val allowed =
                 distinct (op =) (get_starts nts [] @
-                  (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a
+                  (map_filter (fn (_, _, _, Terminal a :: _, _, _) => SOME a
                                | _ => NONE)
                              (Array.sub (stateset, i-1))));
           in syntax_error (if prev_token = EndToken then indata
                            else prev_token :: indata) allowed
           end

           Array.update (stateset, i + 1, sii);
           produce prods chains stateset (i + 1) cs c
        end));
 
 
-fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
+fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
                             l;
 
 fun earley prods tags chains startsymbol indata =
   let
     val start_tag = case Symtab.lookup tags startsymbol of