# HG changeset patch
# User nipkow
# Date 772107928 -7200
# Node ID 0d1071ac599c04631d0a38b47d2c3cce0a7bff40
# Parent  da3d07d4349b20bb822e9879c13b30da6bf37a04
Improved error msg "Proved wrong thm"

diff -r da3d07d4349b -r 0d1071ac599c src/Pure/thm.ML
--- 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 =>