src/Pure/ML/ml_parse.ML
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)