src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/Isar/token.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -183,13 +183,13 @@
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
-fun reset_pos pos (Token ((x, _), y, z)) =
+fun reset_range pos (Token ((x, _), y, z)) =
   let val pos' = Position.reset_range pos
   in Token ((x, (pos', pos')), y, z) end;
 
 fun range_of (toks as tok :: _) =
       let val pos' = end_pos_of (List.last toks)
-      in Position.range (pos_of tok) pos' end
+      in Position.range (pos_of tok, pos') end
   | range_of [] = Position.no_range;
 
 
@@ -666,7 +666,7 @@
 fun make ((k, n), s) pos =
   let
     val pos' = Position.advance_offset n pos;
-    val range = Position.range pos pos';
+    val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then
         Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
@@ -678,7 +678,7 @@
 
 fun make_string (s, pos) =
   #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none)
-  |> reset_pos pos;
+  |> reset_range pos;
 
 fun make_src a args = make_string a :: args;