# HG changeset patch
# User wenzelm
# Date 879348049 -3600
# Node ID 4e0c98184285cbd84227f743a5188f480684d2e7
# Parent  b67223fddc11e2c3b02bdf10c5234e6855b623af
structure BasisLibrary;

diff -r b67223fddc11 -r 4e0c98184285 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Nov 12 16:20:39 1997 +0100
+++ b/src/Pure/ROOT.ML	Wed Nov 12 16:20:49 1997 +0100
@@ -4,11 +4,7 @@
     Copyright   1993  University of Cambridge
 
 Root file for Pure Isabelle: all modules in proper order for loading.
-Loads pure Isabelle into an empty database (see also Makefile).
-
-TO DO:
-instantiation of theorems can lead to inconsistent sorting of type vars if
-'a::S is already present and 'a::T is introduced.
+Loads Pure Isabelle into an empty ML database (see also IsaMakefile).
 *)
 
 val banner = "Pure Isabelle";
@@ -26,6 +22,7 @@
 use "ROOT.ML";
 cd "..";
 
+(*Core system*)
 use "sorts.ML";
 use "type_infer.ML";
 use "type.ML";
@@ -56,4 +53,13 @@
 
 use "install_pp.ML";
 
+(*several object-logics declare theories named List or Option, hiding
+  the eponymous basis library structures*)
+structure BasisLibrary =
+struct
+  structure List = List and Option = Option;
+end;
+
+open Use;
+
 print_depth 8;