1.1 --- a/src/Pure/library.ML	Tue May 20 11:49:57 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Tue May 20 11:53:20 1997 +0200
     1.3 @@ -119,9 +119,10 @@
     1.4  fun andl [] = true
     1.5    | andl (x :: xs) = x andalso andl xs;
     1.6  
     1.7 -(*Needed because several object-logics declare the theory, therefore structure,
     1.8 -  List.*)
     1.9 -structure List_ = List;
    1.10 +(*Several object-logics declare theories named List or Option, hiding the
    1.11 +  eponymous basis library structures.*)
    1.12 +structure List_ = List
    1.13 +and       Option_ = Option;
    1.14  
    1.15  (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
    1.16  fun exists (pred: 'a -> bool) : 'a list -> bool =
    1.17 @@ -742,7 +743,8 @@
    1.18  
    1.19  (*print error message and abort to top level*)
    1.20  
    1.21 -val error_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
    1.22 +val error_fn = ref(fn s => TextIO.output 
    1.23 +		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
    1.24  
    1.25  exception ERROR;
    1.26  fun error msg = (!error_fn msg; raise ERROR);