# HG changeset patch
# User wenzelm
# Date 1000311052 -7200
# Node ID 804ee65ee1a183bf7ee956f098005549e9970b43
# Parent  6a95f3eaa54fed6e43e62f992d6d76ca1ae3f351
result_error_default: include msg;

diff -r 6a95f3eaa54f -r 804ee65ee1a1 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Sep 11 15:36:16 2001 +0200
+++ b/src/Pure/goals.ML	Wed Sep 12 18:10:52 2001 +0200
@@ -132,7 +132,7 @@
   special applications.*)
 fun result_error_default state msg : thm =
   Pretty.str "Bad final proof state:" :: pretty_goals (!goals_limit) state @
-    [Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
+    [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
 
 val result_error_fn = ref result_error_default;