# HG changeset patch # User wenzelm # Date 1389988296 -3600 # Node ID b493662154173cd4713f35f7c1113052aa308c32 # Parent e58066daa065e7eaedd12cbe208b820e656ae225 back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally; diff -r e58066daa065 -r b49366215417 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Jan 17 20:36:57 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Fri Jan 17 20:51:36 2014 +0100 @@ -856,8 +856,8 @@ let val _ $ _ $ prop0 = Thm.prop_of thm; val _ = - warning - (print_thm ctxt "Simplifier: proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^ + cond_tracing ctxt (fn () => + print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^ print_term ctxt "Should have proved:" prop0); in NONE end;