src/Pure/ROOT.ML
changeset 2 c67f44be880f
parent 0 a5a9c433f639
child 19 929ad32d63fc
     1.1 --- a/src/Pure/ROOT.ML	Thu Sep 16 14:21:44 1993 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu Sep 16 16:25:32 1993 +0200
     1.3 @@ -28,11 +28,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  print_depth 1;
    1.13  use "type.ML";
    1.14  use "sign.ML";
    1.15 @@ -69,3 +64,9 @@
    1.16  open Basic_Syntax Thm Drule Tactical Tactic Goals;
    1.17  
    1.18  structure Pure = struct val thy = pure_thy end;
    1.19 +
    1.20 +(* Theory parser *)
    1.21 +cd "Thy";
    1.22 +use "ROOT.ML";
    1.23 +cd "..";
    1.24 +