--- 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;