# HG changeset patch
# User wenzelm
# Date 1163635659 -3600
# Node ID afd8ba74313cfa8d2b779b0000438f010cdee70b
# Parent  f34ac19659aea0d51e03fc376fb40adcd7943050
added General/basics.ML;

diff -r f34ac19659ae -r afd8ba74313c src/Pure/ROOT.ML
--- 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 "..";