tuned error msg;

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