# HG changeset patch
# User wenzelm
# Date 1222346101 -7200
# Node ID b9d9360e24402916152b0ffe88aa92bc0b82f636
# Parent  c5fe7372ae4e7a45d4adaad4ef4853c485664c27
prove: error with original thread position;

diff -r c5fe7372ae4e -r b9d9360e2440 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Sep 25 13:21:13 2008 +0200
+++ b/src/Pure/goal.ML	Thu Sep 25 14:35:01 2008 +0200
@@ -147,9 +147,11 @@
     val thy = ProofContext.theory_of ctxt;
     val string_of_term = Syntax.string_of_term ctxt;
 
+    val pos = Position.thread_data ();
     fun err msg = cat_error msg
       ("The error(s) above occurred for the goal statement:\n" ^
-        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
+        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
+        (case Position.str_of pos of "" => "" | s => "\n" ^ s));
 
     fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;