src/Pure/General/position.ML
changeset 72707 f1380c9f3806
parent 72706 52d0b5fcb19d
child 73864 ac5a72740f3a
--- a/src/Pure/General/position.ML	Wed Nov 25 13:51:28 2020 +0100
+++ b/src/Pure/General/position.ML	Wed Nov 25 15:12:02 2020 +0100
@@ -90,7 +90,7 @@
 
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
-    Markup.position_properties';
+    [Markup.fileN, Markup.idN];
 
 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};