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 ".."; +