diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/General/position.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -41,7 +41,7 @@
   val reports_text: report_text list -> unit
   val reports: report list -> unit
   val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
-  val str_of: T -> string
+  val here: T -> string
   type range = T * T
   val no_range: range
   val set_range: range -> T
@@ -180,9 +180,9 @@
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
 
 
-(* str_of *)
+(* here: inlined formal markup *)
 
-fun str_of pos =
+fun here pos =
   let
     val props = properties_of pos;
     val s =