tuned signature;

--- a/src/Pure/General/antiquote.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/General/antiquote.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -37,7 +37,7 @@
 
 fun range ants =
   if null ants then Position.no_range
-  else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants)));
+  else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
 
 
 (* split lines *)
@@ -110,9 +110,9 @@
     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
       (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
     (fn (pos1, (pos2, ((body, pos3), pos4))) =>
-      {start = Position.set_range (pos1, pos2),
-       stop = Position.set_range (pos3, pos4),
-       range = Position.range pos1 pos4,
+      {start = Position.range_position (pos1, pos2),
+       stop = Position.range_position (pos3, pos4),
+       range = Position.range (pos1, pos4),
        body = body});
 
 val scan_antiquote =

--- a/src/Pure/General/position.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/General/position.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -51,9 +51,9 @@
   val here_list: T list -> string
   type range = T * T
   val no_range: range
-  val set_range: range -> T
+  val range_position: range -> T
+  val range: T * T -> range
   val reset_range: T -> T
-  val range: T -> T -> range
   val range_of_properties: Properties.T -> range
   val properties_of_range: range -> Properties.T
   val thread_data: unit -> T
@@ -223,11 +223,11 @@
 
 val no_range = (none, none);
 
-fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
+fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
+fun range (pos, pos') = (range_position (pos, pos'), pos');
+
 fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
 
-fun range pos pos' = (set_range (pos, pos'), pos');
-
 fun range_of_properties props =
   let
     val pos = of_properties props;

--- a/src/Pure/General/symbol_pos.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/General/symbol_pos.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -63,7 +63,7 @@
 
 fun range (syms as (_, pos) :: _) =
       let val pos' = List.last syms |-> Position.advance
-      in Position.range pos pos' end
+      in Position.range (pos, pos') end
   | range [] = Position.no_range;
 
 

--- 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;
 

--- a/src/Pure/ML/ml_lex.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -312,7 +312,7 @@
         let
           val pos1 = List.last syms |-> Position.advance;
           val pos2 = Position.advance Symbol.space pos1;
-        in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
+        in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
 
     val scan = if SML then scan_sml else scan_ml_antiq;
     fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)

--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -71,7 +71,7 @@
   | range_of (Binder (_, _, _, range)) = range
   | range_of (Structure range) = range;
 
-val pos_of = Position.set_range o range_of;
+val pos_of = Position.range_position o range_of;
 
 fun reset_pos NoSyn = NoSyn
   | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)

--- a/src/Pure/Tools/rail.ML	Fri Apr 01 17:23:15 2016 +0200
+++ b/src/Pure/Tools/rail.ML	Fri Apr 01 17:37:46 2016 +0200
@@ -53,7 +53,7 @@
 
 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;
 
 fun kind_of (Token (_, (k, _))) = k;
@@ -116,7 +116,7 @@
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
   Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
-    [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
+    [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
 
 val scan =
   Scan.repeats scan_token --|
@@ -188,7 +188,7 @@
     let
       fun reports r =
         if r = Position.no_range then []
-        else [(Position.set_range r, Markup.expression)];
+        else [(Position.range_position r, Markup.expression)];
       fun trees (CAT (ts, r)) = reports r @ maps tree ts
       and tree (BAR (Ts, r)) = reports r @ maps trees Ts
         | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2