diff -r 39aeccee9e1c -r 09966ccbc84c src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Mon Nov 19 17:40:07 2001 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Mon Nov 19 17:40:45 2001 +0100
@@ -45,7 +45,9 @@
             val thm = lookup name;
             val {prop, ...} = rep_thm thm;
             val _ = if prop=prop' then () else
-              error ("Duplicate use of theorem name " ^ quote name);
+              error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+                Sign.string_of_term sg prop ^ "\n\n" ^
+                Sign.string_of_term sg prop');
             val tvars = term_tvars prop;
             val ctye = map fst tvars ~~ map (Thm.ctyp_of sg) Ts
           in