moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
authorclasohm
Thu, 16 Sep 1993 16:25:32 +0200
changeset 2 c67f44be880f
parent 1 c6a6e3db5353
child 3 5f77582e3a89
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Sep 16 14:21:44 1993 +0200
+++ b/src/Pure/ROOT.ML	Thu Sep 16 16:25:32 1993 +0200
@@ -28,11 +28,6 @@
 use "ROOT.ML";
 cd "..";
 
-(* Theory parser *)
-cd "Thy";
-use "ROOT.ML";
-cd "..";
-
 print_depth 1;
 use "type.ML";
 use "sign.ML";
@@ -69,3 +64,9 @@
 open Basic_Syntax Thm Drule Tactical Tactic Goals;
 
 structure Pure = struct val thy = pure_thy end;
+
+(* Theory parser *)
+cd "Thy";
+use "ROOT.ML";
+cd "..";
+