src/Pure/ROOT.ML
changeset 73 075db6ac7f2f
parent 19 929ad32d63fc
child 83 de9316670e89
--- a/src/Pure/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
+++ b/src/Pure/ROOT.ML	Fri Oct 22 13:39:23 1993 +0100
@@ -27,11 +27,6 @@
 use "ROOT.ML";
 cd "..";
 
-(*Theory parser*)
-cd "Thy";
-use "ROOT.ML";
-cd "..";
-
 use "type.ML";
 use "sign.ML";
 use "sequence.ML";
@@ -70,3 +65,12 @@
 
 use "install_pp.ML";
 
+
+
+(*Theory parser
+  (The new Thy/read.ML needs Thm so this has to be done AFTER Thm is
+   created.) *)
+cd "Thy";
+use "ROOT.ML";
+cd "..";
+