# HG changeset patch
# User wenzelm
# Date 895683341 -7200
# Node ID c73f72daee64559c037ff1225db6376666c6d5b6
# Parent  c53aa26ccfd217bee908179901fd49c4307ce812
tuned comments;

diff -r c53aa26ccfd2 -r c73f72daee64 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed May 20 18:55:16 1998 +0200
+++ b/src/Pure/ROOT.ML	Wed May 20 18:55:41 1998 +0200
@@ -12,18 +12,20 @@
 
 print_depth 1;
 
+
+(*basic utils*)
 use "library.ML";
 use "table.ML";
 use "seq.ML";
 use "name_space.ML";
 use "term.ML";
 
-(*Syntax module*)
+(*inner syntax module*)
 cd "Syntax";
 use "ROOT.ML";
 cd "..";
 
-(*Main system*)
+(*main system*)
 use "sorts.ML";
 use "type_infer.ML";
 use "type.ML";
@@ -46,7 +48,7 @@
 use "goals.ML";
 use "axclass.ML";
 
-(*Theory parser and loader*)
+(*theory parser and loader*)
 val global_names = ref false;		(* FIXME tmp *)
 cd "Thy";
 use "ROOT.ML";