src/Pure/ROOT.ML
changeset 73 075db6ac7f2f
parent 19 929ad32d63fc
child 83 de9316670e89
     1.1 --- a/src/Pure/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Oct 22 13:39:23 1993 +0100
     1.3 @@ -27,11 +27,6 @@
     1.4  use "ROOT.ML";
     1.5  cd "..";
     1.6  
     1.7 -(*Theory parser*)
     1.8 -cd "Thy";
     1.9 -use "ROOT.ML";
    1.10 -cd "..";
    1.11 -
    1.12  use "type.ML";
    1.13  use "sign.ML";
    1.14  use "sequence.ML";
    1.15 @@ -70,3 +65,12 @@
    1.16  
    1.17  use "install_pp.ML";
    1.18  
    1.19 +
    1.20 +
    1.21 +(*Theory parser
    1.22 +  (The new Thy/read.ML needs Thm so this has to be done AFTER Thm is
    1.23 +   created.) *)
    1.24 +cd "Thy";
    1.25 +use "ROOT.ML";
    1.26 +cd "..";
    1.27 +