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;