src/Pure/ROOT.ML
changeset 5568 0067dd151d7a
parent 5244 5313f781efe0
child 5607 5db9e2343ade
     1.1 --- a/src/Pure/ROOT.ML	Fri Sep 25 14:06:00 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Sep 25 14:06:27 1998 +0200
     1.3 @@ -60,11 +60,12 @@
     1.4  (*if true then some packages won't be too serious about actually proving things*)
     1.5  val quick_and_dirty = ref false;
     1.6  
     1.7 -(*several object-logics declare theories named List or Option, hiding
     1.8 -  the eponymous basis library structures*)
     1.9 +(*several object-logics declare theories that hide basis library structures*)
    1.10  structure BasisLibrary =
    1.11  struct
    1.12 -  structure List = List and Option = Option;
    1.13 +  structure List   = List 
    1.14 +  and       Option = Option
    1.15 +  and       Int    = Int;
    1.16  end;
    1.17  
    1.18  open Use;