# HG changeset patch
# User wenzelm
# Date 1284736303 -7200
# Node ID 73bcb12fdc69643b035539abd6257246b3f16e5e
# Parent  4110cc1b8f9f135d88ae15590ee30e68c3d29360
tuned;

diff -r 4110cc1b8f9f -r 73bcb12fdc69 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Sep 17 17:10:44 2010 +0200
+++ b/src/Pure/General/binding.ML	Fri Sep 17 17:11:43 2010 +0200
@@ -124,10 +124,8 @@
 (* str_of *)
 
 fun str_of binding =
-  let
-    val text = qualified_name_of binding;
-    val props = Position.properties_of (pos_of binding);
-  in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
+  qualified_name_of binding
+  |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
 
 end;
 end;