Improved error msg "Proved wrong thm"

--- a/src/Pure/thm.ML	Mon Jun 20 12:13:08 1994 +0200
+++ b/src/Pure/thm.ML	Mon Jun 20 12:25:28 1994 +0200
@@ -1192,8 +1192,10 @@
 
 fun termless tu = (termord tu = LESS);
 
-fun check_conv(thm as Thm{hyps,prop,...}, prop0) =
-  let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)
+fun check_conv(thm as Thm{hyps,prop,sign,...}, prop0) =
+  let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm;
+                   trace_term "Should have proved" sign prop0;
+                   None)
       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
   in case prop of
        Const("==",_) $ lhs $ rhs =>