diff -r d9ea690001ce -r b96a26593532 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 07 10:38:04 2000 +0200
+++ b/src/Pure/thm.ML	Thu Sep 07 15:31:09 2000 +0200
@@ -2147,12 +2147,12 @@
                      prop = prop',
                      maxidx = maxidx'};
       val unit = trace_thm false "Applying congruence rule:" thm';
-      fun err() = error("Failed congruence proof!")
+      fun err(msg,thm) = (prthm false msg thm; error("Failed congruence proof!"))
 
   in case prover thm' of
-       None => err()
+       None => err("Could not prove",thm')
      | Some(thm2) => (case check_conv(thm2,prop',ders) of
-                        None => err() | Some trec => trec)
+                        None => err("Should not have proved",thm2) | Some trec => trec)
   end;
 
 fun bottomc ((simprem,useprem,mutsimp),prover,sign_ref,maxidx) =