tuned;
authorwenzelm
Wed, 02 Oct 2013 19:49:15 +0200
changeset 54038 f522477d671d
parent 54037 ab77ec347220
child 54039 c931190b8c5c
tuned;
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