src/Pure/library.ML

   | orl (x :: xs) = x orelse orl xs;
 
 fun andl [] = true
   | andl (x :: xs) = x andalso andl xs;
 
-(*Needed because several object-logics declare the theory, therefore structure,
-  List.*)
-structure List_ = List;
+(*Several object-logics declare theories named List or Option, hiding the
+  eponymous basis library structures.*)
+structure List_ = List
+and       Option_ = Option;
 
 (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
 fun exists (pred: 'a -> bool) : 'a list -> bool =
   let fun boolf [] = false
         | boolf (x :: xs) = pred x orelse boolf xs

 val warning_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
 fun warning s = !warning_fn ("Warning: " ^ s);
 
 (*print error message and abort to top level*)
 
-val error_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
+val error_fn = ref(fn s => TextIO.output 
+		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
 
 exception ERROR;
 fun error msg = (!error_fn msg; raise ERROR);
 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);