# HG changeset patch
# User wenzelm
# Date 1288302879 -7200
# Node ID bb433b0668b898acaaea1734e8a61af86559dd8d
# Parent  56fad09655a5079ca1b0ace201b01830066125c6
tuned messages;

diff -r 56fad09655a5 -r bb433b0668b8 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Oct 28 23:19:52 2010 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Oct 28 23:54:39 2010 +0200
@@ -44,8 +44,9 @@
 
 fun cert_def ctxt eq =
   let
-    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
-      quote (Syntax.string_of_term ctxt eq));
+    fun err msg =
+      cat_error msg ("The error(s) above occurred in definition:\n" ^
+        quote (Syntax.string_of_term ctxt eq));
     val ((lhs, _), eq') = eq
       |> Sign.no_vars ctxt
       |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
@@ -245,7 +246,7 @@
           (CONVERSION (meta_rewrite_conv ctxt') THEN'
             MetaSimplifier.rewrite_goal_tac [def] THEN'
             resolve_tac [Drule.reflexive_thm])))
-        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
+        handle ERROR msg => cat_error msg "Failed to prove definitional specification"
       end;
   in (((c, T), rhs), prove) end;