# HG changeset patch
# User wenzelm
# Date 1392751978 -3600
# Node ID d4aea4bbe87fd8fa9a7d78459ad749a94b8f2fe1
# Parent  298274c970b6e039f9eecc9da614330411d6f996
tuned message;

diff -r 298274c970b6 -r d4aea4bbe87f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Feb 18 20:20:42 2014 +0100
+++ b/src/Pure/goal.ML	Tue Feb 18 20:32:58 2014 +0100
@@ -187,10 +187,10 @@
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
-    fun err msg = cat_error msg
-      ("The error(s) above occurred for the goal statement:\n" ^
-        Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
-        (case Position.here pos of "" => "" | s => "\n" ^ s));
+    fun err msg =
+      cat_error msg
+        ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^
+          Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
 
     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;