changeset 48911 | 5debc3e4fa81 |
parent 47297 | de84dd9a9dd4 |
child 48992 | 0518bf89c777 |
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Thu Aug 23 17:46:03 2012 +0200 @@ -191,7 +191,7 @@ fun !!! text scan = let - fun get_pos [] = " (past end-of-text!)" + fun get_pos [] = " (end-of-input)" | get_pos ((_, pos) :: _) = Position.str_of pos; fun err (syms, msg) = fn () =>