src/Pure/General/position.ML
changeset 62800 7ac100f86863
parent 62798 2948681ea85f
child 62803 5f73bf6ba98b
--- a/src/Pure/General/position.ML	Fri Apr 01 17:49:03 2016 +0200
+++ b/src/Pure/General/position.ML	Fri Apr 01 17:56:14 2016 +0200
@@ -51,7 +51,7 @@
   val here_list: T list -> string
   type range = T * T
   val no_range: range
-  val reset_range: T -> T
+  val no_range_position: T -> T
   val range_position: range -> T
   val range: T * T -> range
   val range_of_properties: Properties.T -> range
@@ -223,9 +223,9 @@
 
 val no_range = (none, none);
 
-fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
+fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
 fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
-fun range (pos, pos') = (range_position (pos, pos'), reset_range pos');
+fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
 
 fun range_of_properties props =
   let