src/Pure/library.ML
changeset 3874 552ce5ad6a2e
parent 3832 17a20a2af8f5
child 3973 1be726ef6813
     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