1.1 --- a/src/Pure/ROOT.ML	Wed Nov 12 16:20:39 1997 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Nov 12 16:20:49 1997 +0100
     1.3 @@ -4,11 +4,7 @@
     1.4      Copyright   1993  University of Cambridge
     1.5  
     1.6  Root file for Pure Isabelle: all modules in proper order for loading.
     1.7 -Loads pure Isabelle into an empty database (see also Makefile).
     1.8 -
     1.9 -TO DO:
    1.10 -instantiation of theorems can lead to inconsistent sorting of type vars if
    1.11 -'a::S is already present and 'a::T is introduced.
    1.12 +Loads Pure Isabelle into an empty ML database (see also IsaMakefile).
    1.13  *)
    1.14  
    1.15  val banner = "Pure Isabelle";
    1.16 @@ -26,6 +22,7 @@
    1.17  use "ROOT.ML";
    1.18  cd "..";
    1.19  
    1.20 +(*Core system*)
    1.21  use "sorts.ML";
    1.22  use "type_infer.ML";
    1.23  use "type.ML";
    1.24 @@ -56,4 +53,13 @@
    1.25  
    1.26  use "install_pp.ML";
    1.27  
    1.28 +(*several object-logics declare theories named List or Option, hiding
    1.29 +  the eponymous basis library structures*)
    1.30 +structure BasisLibrary =
    1.31 +struct
    1.32 +  structure List = List and Option = Option;
    1.33 +end;
    1.34 +
    1.35 +open Use;
    1.36 +
    1.37  print_depth 8;