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)