src/Pure/ROOT.ML
changeset 3986 d788dcb86930
parent 3971 b19d38604042
child 4209 4e0c98184285
     1.1 --- a/src/Pure/ROOT.ML	Fri Oct 24 17:06:45 1997 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Oct 24 17:07:34 1997 +0200
     1.3 @@ -39,8 +39,9 @@
     1.4  use "logic.ML";
     1.5  use "theory.ML";
     1.6  use "thm.ML";
     1.7 +use "display.ML";
     1.8 +use "pure_thy.ML";
     1.9  use "deriv.ML";
    1.10 -use "display.ML";
    1.11  use "drule.ML";
    1.12  use "tctical.ML";
    1.13  use "search.ML";
    1.14 @@ -48,9 +49,6 @@
    1.15  use "goals.ML";
    1.16  use "axclass.ML";
    1.17  
    1.18 -structure Pure  = struct val thy = Theory.pure end;
    1.19 -structure CPure = struct val thy = Theory.cpure end;
    1.20 -
    1.21  (*Theory parser and loader*)
    1.22  cd "Thy";
    1.23  use "ROOT.ML";