src/Pure/ROOT.ML
changeset 4949 c73f72daee64
parent 4781 6b55d02437ad
child 4962 e9217cb15b42
     1.1 --- a/src/Pure/ROOT.ML	Wed May 20 18:55:16 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed May 20 18:55:41 1998 +0200
     1.3 @@ -12,18 +12,20 @@
     1.4  
     1.5  print_depth 1;
     1.6  
     1.7 +
     1.8 +(*basic utils*)
     1.9  use "library.ML";
    1.10  use "table.ML";
    1.11  use "seq.ML";
    1.12  use "name_space.ML";
    1.13  use "term.ML";
    1.14  
    1.15 -(*Syntax module*)
    1.16 +(*inner syntax module*)
    1.17  cd "Syntax";
    1.18  use "ROOT.ML";
    1.19  cd "..";
    1.20  
    1.21 -(*Main system*)
    1.22 +(*main system*)
    1.23  use "sorts.ML";
    1.24  use "type_infer.ML";
    1.25  use "type.ML";
    1.26 @@ -46,7 +48,7 @@
    1.27  use "goals.ML";
    1.28  use "axclass.ML";
    1.29  
    1.30 -(*Theory parser and loader*)
    1.31 +(*theory parser and loader*)
    1.32  val global_names = ref false;		(* FIXME tmp *)
    1.33  cd "Thy";
    1.34  use "ROOT.ML";