src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Mon Feb 24 10:17:29 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Feb 24 10:48:34 2014 +0100
@@ -17,7 +17,7 @@
   type T
   val str_of_kind: kind -> string
   val pos_of: T -> Position.T
-  val position_range_of: T list -> Position.range
+  val range_of: T list -> Position.range
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -131,8 +131,10 @@
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
-fun position_range_of [] = Position.no_range
-  | position_range_of toks = (pos_of (hd toks), end_pos_of (List.last toks));
+fun range_of (toks as tok :: _) =
+      let val pos' = end_pos_of (List.last toks)
+      in Position.range (pos_of tok) pos' end
+  | range_of [] = Position.no_range;
 
 
 (* control tokens *)