src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -279,7 +279,7 @@
       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;