src/Pure/General/position.ML

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