diff -r e8b1c3a0562c -r 1c8cf0048934 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon May 31 16:45:48 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon May 31 18:17:48 2010 +0200
@@ -87,11 +87,7 @@
           map (pair (offset_of p)) (String.explode (Symbol.esc sym)))
       end);
 
-    val end_pos =
-      if null toks then Position.none
-      else ML_Lex.end_pos_of (List.last toks);
-
-    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+    val input_buffer = Unsynchronized.ref input;
     val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
 
     fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);