# HG changeset patch
# User wenzelm
# Date 1459525743 -7200
# Node ID 46e6f91c4da1fdd98a072a2df39111ba3e46cfa7
# Parent  2948681ea85f83bb975d940b1f4d1e43cd356dbd
tuned;

diff -r 2948681ea85f -r 46e6f91c4da1 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Apr 01 17:41:41 2016 +0200
+++ b/src/Pure/Isar/token.ML	Fri Apr 01 17:49:03 2016 +0200
@@ -183,10 +183,6 @@
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
-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
@@ -677,8 +673,10 @@
   in (tok, pos') end;
 
 fun make_string (s, pos) =
-  #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none)
-  |> reset_range pos;
+  let
+    val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none);
+    val pos' = Position.reset_range pos;
+  in Token ((x, (pos', pos')), y, z) end;
 
 fun make_src a args = make_string a :: args;