src/Pure/Syntax/mixfix.ML
changeset 62797 e08c44eed27f
parent 62796 99f2036f37af
child 62959 19c2a58623ed
--- 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)