diff -r 5d142ca01b8e -r 0f3537fad0f3 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Dec 27 18:27:49 2000 +0100
+++ b/src/Pure/goals.ML	Fri Dec 29 19:43:52 2000 +0100
@@ -133,7 +133,7 @@
 fun result_error_default state msg : thm =
  (writeln "Bad final proof state:";
   print_goals (!goals_limit) state;
-  writeln msg; raise ERROR);
+  writeln msg; error "Proof failed");
 
 val result_error_fn = ref result_error_default;