# HG changeset patch
# User wenzelm
# Date 1257179388 -3600
# Node ID b834b42e4aa1d5e6aad880a38674d74d50f207e4
# Parent  c394abc5f898ce77017f0b9a5269efc7f79d4135
back to warning -- Proof General tends to "popup" tracing output;

diff -r c394abc5f898 -r b834b42e4aa1 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Nov 02 15:49:59 2009 +0100
+++ b/src/Pure/meta_simplifier.ML	Mon Nov 02 17:29:48 2009 +0100
@@ -1025,7 +1025,7 @@
                  val b' = #1 (Term.dest_Free (Thm.term_of v));
                  val _ =
                    if b <> b' then
-                     tracing ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
+                     warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
                    else ();
                  val ss' = add_bound ((b', T), a) ss;
                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;