# HG changeset patch
# User wenzelm
# Date 1459277539 -7200
# Node ID 3f8f7aa1b11ec76c312671abbe1d69d236df975c
# Parent  eba34ff9671c647582ac79e8d588a83ed81e1fbf
proper norm_props, e.g. relevant for ML pp;

diff -r eba34ff9671c -r 3f8f7aa1b11e src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Mar 29 16:20:48 2016 +0200
+++ b/src/Pure/General/position.ML	Tue Mar 29 20:52:19 2016 +0200
@@ -135,7 +135,7 @@
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
-fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
+fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
 
 fun parse_id pos = Option.map Markup.parse_int (get_id pos);