tuned;
authorwenzelm
Fri, 01 Apr 2016 17:49:03 +0200
changeset 62799 46e6f91c4da1
parent 62798 2948681ea85f
child 62800 7ac100f86863
tuned;
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;