# HG changeset patch
# User wenzelm
# Date 1314036004 -7200
# Node ID c38bb61deeaa4b8e65ef62c044de9bb483c0dc30
# Parent  1b1afb1380ee18667f47172d536161efb17e00ca
tuned message;

diff -r 1b1afb1380ee -r c38bb61deeaa src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Mon Aug 22 17:10:22 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Aug 22 20:00:04 2011 +0200
@@ -260,11 +260,12 @@
           let
             val x = the_struct structs n;
             val advice =
-              if n = 1 then " -- may be omitted"
-              else " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead";
+              " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+              (if n = 1 then " (may be omitted)" else "");
             val _ =
               legacy_feature
-                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^ advice);
+                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
+                  Position.str_of (Position.thread_data ()) ^ advice);
           in Syntax.free x end
       | NONE => raise TERM ("struct_tr", [t]))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);