diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/Isar/token.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -130,7 +130,7 @@
 fun position_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
 
-val pos_of = Position.str_of o position_of;
+val pos_of = Position.here o position_of;
 
 
 (* control tokens *)
@@ -244,7 +244,7 @@
 
 fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
   | put_files _ tok =
-      raise Fail ("Cannot put inlined files here" ^ Position.str_of (position_of tok));
+      raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
 
 
 (* access values *)
@@ -402,7 +402,7 @@
 
 fun read_antiq lex scan (syms, pos) =
   let
-    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
+    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
       "@{" ^ Symbol_Pos.content syms ^ "}");
 
     val res =