back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
authorwenzelm
Fri Jan 17 20:51:36 2014 +0100 (2014-01-17)
changeset 55032b49366215417
parent 55031 e58066daa065
child 55033 8e8243975860
back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Jan 17 20:36:57 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Jan 17 20:51:36 2014 +0100
     1.3 @@ -856,8 +856,8 @@
     1.4      let
     1.5        val _ $ _ $ prop0 = Thm.prop_of thm;
     1.6        val _ =
     1.7 -        warning
     1.8 -         (print_thm ctxt "Simplifier: proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^
     1.9 +        cond_tracing ctxt (fn () =>
    1.10 +          print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^
    1.11            print_term ctxt "Should have proved:" prop0);
    1.12      in NONE end;
    1.13