# HG changeset patch
# User wenzelm
# Date 1380736155 -7200
# Node ID f522477d671d8df89498a92e0380bd701576e940
# Parent  ab77ec3472202a2307d29d05f4dbe3c94957b1d5
tuned;

diff -r ab77ec347220 -r f522477d671d src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Oct 02 19:43:58 2013 +0200
+++ b/src/Pure/General/position.ML	Wed Oct 02 19:49:15 2013 +0200
@@ -146,7 +146,7 @@
 fun properties_of (Pos ((i, j, k), props)) =
   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
 
-val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
+val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
 
 fun entity_properties_of def id pos =
   if def then (Markup.defN, Markup.print_int id) :: properties_of pos