tuned;
authorwenzelm
Fri, 17 Sep 2010 17:11:43 +0200
changeset 39442 73bcb12fdc69
parent 39441 4110cc1b8f9f
child 39506 cf61ec140c4d
tuned;
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;