src/Pure/Syntax/lexicon.ML

       Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => SOME (tk s)) ||
       scan_str >> (SOME o StrSy o implode_xstr) ||
       Scan.one Symbol.is_blank >> K NONE;
   in
     (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
-      (toks, []) => List.mapPartial I toks @ [EndToken]
+      (toks, []) => map_filter I toks @ [EndToken]
     | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
   end;