# HG changeset patch
# User wenzelm
# Date 1266576971 -3600
# Node ID 98e52f522357e128f041b7616076739efefbe475
# Parent  be006fbcfb96e45a666a4c2c41a69416d86e827c
tuned message;

diff -r be006fbcfb96 -r 98e52f522357 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Feb 19 11:49:44 2010 +0100
+++ b/src/Pure/meta_simplifier.ML	Fri Feb 19 11:56:11 2010 +0100
@@ -1025,7 +1025,8 @@
                  val b' = #1 (Term.dest_Free (Thm.term_of v));
                  val _ =
                    if b <> b' then
-                     warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
+                     warning ("Simplifier: renamed bound variable " ^
+                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
                    else ();
                  val ss' = add_bound ((b', T), a) ss;
                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;