diff -r fd341ca4b8de -r 0ae32184bde0 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sat Jun 06 19:58:10 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sat Jun 06 19:58:11 2009 +0200
@@ -15,6 +15,7 @@
   val is_improper: token -> bool
   val set_range: Position.range -> token -> token
   val pos_of: token -> Position.T
+  val end_pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
   val check_content_of: token -> string