# 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;