src/Pure/raw_simplifier.ML
changeset 55032 b49366215417
parent 55031 e58066daa065
child 55316 885500f4aa6a
     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