# HG changeset patch
# User wenzelm
# Date 1129651176 -7200
# Node ID 4d7fe1816ab13daee149ab2a0221ad48c09ae14e
# Parent  7b35ce796a4d18bd38edffb8206a07496ce5a207
tuned error msg;

diff -r 7b35ce796a4d -r 4d7fe1816ab1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 18 17:59:35 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 18 17:59:36 2005 +0200
@@ -485,7 +485,7 @@
     conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
         cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
     conditional (exists (not o Pattern.matches thy) (props ~~ map Thm.prop_of ths)) (fn () =>
-      err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th)));
+      err ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
     ths
   end;