--- 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