--- a/src/Pure/ROOT.ML Thu Nov 16 01:07:25 2006 +0100 +++ b/src/Pure/ROOT.ML Thu Nov 16 01:07:39 2006 +0100 @@ -16,6 +16,7 @@ structure Hidden = struct end; (*basic tools*) +use "General/basics.ML"; use "library.ML"; cd "General"; use "ROOT.ML"; cd "..";