changeset 48911 | 5debc3e4fa81 |
parent 48770 | 85eeb06ec1c4 |
child 48992 | 0518bf89c777 |
--- a/src/Pure/General/symbol_pos.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/General/symbol_pos.ML Thu Aug 23 17:46:03 2012 +0200 @@ -66,7 +66,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 () =>