changeset 48911 | 5debc3e4fa81 |
parent 43948 | 8f5add916a99 |
child 48992 | 0518bf89c777 |
--- a/src/Pure/ML/ml_parse.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/ML/ml_parse.ML Thu Aug 23 17:46:03 2012 +0200 @@ -17,7 +17,7 @@ fun !!! scan = let - fun get_pos [] = " (past end-of-file!)" + fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok); fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)