# HG changeset patch
# User wenzelm
# Date 999972314 -7200
# Node ID 685daff01da4203a71e0404783b2adb03e55a915
# Parent  87b585079d01f7f0a8aff2242cda18c6326ec9e1
result_error_default: output *single* error message;

diff -r 87b585079d01 -r 685daff01da4 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Sat Sep 08 20:03:22 2001 +0200
+++ b/src/Pure/goals.ML	Sat Sep 08 20:05:14 2001 +0200
@@ -131,9 +131,8 @@
 (*Default action is to print an error message; could be suppressed for
   special applications.*)
 fun result_error_default state msg : thm =
- (writeln "Bad final proof state:";
-  print_goals (!goals_limit) state;
-  writeln msg; error "Proof failed");
+  Pretty.str "Bad final proof state:" :: pretty_goals (!goals_limit) state @
+    [Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
 
 val result_error_fn = ref result_error_default;