back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;

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