changeset 33336 | cd53fa891be5 |
parent 33245 | 65232054ffd0 |
child 33379 | b834b42e4aa1 |
--- a/src/Pure/meta_simplifier.ML Thu Oct 29 20:35:47 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Thu Oct 29 20:53:24 2009 +0100 @@ -1025,7 +1025,7 @@ 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') + tracing ("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;