src/HOL/SPARK/Tools/fdl_lexer.ML

       |> implode) ^ dots
   end;
 
 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 () =>
       text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^
         (case msg of NONE => "" | SOME m => "\n" ^ m ());