src/Pure/ML/ml_lex.ML

--- a/src/Pure/ML/ml_lex.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/ML/ml_lex.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -82,7 +82,7 @@
     Token (_, (Keyword, ":>")) =>
       warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
         \prefer non-opaque matching (:) possibly with abstype" ^
-        Position.str_of (pos_of tok))
+        Position.here (pos_of tok))
   | _ => ());
 
 fun check_content_of tok =
@@ -307,7 +307,7 @@
         |> tap Antiquote.check_nesting
         |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
       handle ERROR msg =>
-        cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+        cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
   in input @ termination end;
 
 end;