author | wenzelm |
Wed, 15 Oct 1997 15:13:43 +0200 | |
changeset 3874 | 552ce5ad6a2e |
parent 3873 | 64f496e0885d |
child 3875 | f62a4edb1888 |
--- a/src/Pure/library.ML Wed Oct 15 15:13:25 1997 +0200 +++ b/src/Pure/library.ML Wed Oct 15 15:13:43 1997 +0200 @@ -770,7 +770,7 @@ (*print error message and abort to top level*) exception ERROR; -fun error_msg s = !error_fn s; +fun error_msg s = !error_fn s; (*promise to raise ERROR later!*) fun error s = (error_msg s; raise ERROR); fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);