# HG changeset patch
# User paulson
# Date 864122000 -7200
# Node ID 7f783705c7a4dd0a3398d014e4791196b1a31236
# Parent  241838c01cafa0c01f5bc86a953ffa8f79765c64
Declares Option_ as synonym for structure Option

diff -r 241838c01caf -r 7f783705c7a4 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue May 20 11:49:57 1997 +0200
+++ b/src/Pure/library.ML	Tue May 20 11:53:20 1997 +0200
@@ -119,9 +119,10 @@
 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 =
@@ -742,7 +743,8 @@
 
 (*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);