| changeset 10745 | 0f3537fad0f3 |
| parent 10487 | 97d25c125c61 |
| child 11554 | 685daff01da4 |
--- 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;