--- a/src/Pure/goals.ML Sat Jul 10 21:34:01 1999 +0200
+++ b/src/Pure/goals.ML Sat Jul 10 21:35:08 1999 +0200
@@ -275,8 +275,8 @@
| _ => error ("prove_goal: tactic failed"))
in mkresult (check, cond_timeit (!proof_timing) statef) end
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
- error ("The exception above was raised for\n" ^
- string_of_cterm chorn));
+ writeln ("The exception above was raised for\n" ^
+ string_of_cterm chorn); raise e);
(*Two variants: one checking the result, one not.
Neither prints runtime messages: they are for internal packages.*)