tuned comment;
authorwenzelm
Wed Oct 15 15:13:43 1997 +0200 (1997-10-15)
changeset 3874552ce5ad6a2e
parent 3873 64f496e0885d
child 3875 f62a4edb1888
tuned comment;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Oct 15 15:13:25 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Oct 15 15:13:43 1997 +0200
     1.3 @@ -770,7 +770,7 @@
     1.4  
     1.5  (*print error message and abort to top level*)
     1.6  exception ERROR;
     1.7 -fun error_msg s = !error_fn s;
     1.8 +fun error_msg s = !error_fn s;			(*promise to raise ERROR later!*)
     1.9  fun error s = (error_msg s; raise ERROR);
    1.10  fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);
    1.11