added init_database (somewhat experimental);
authorwenzelm
Mon Sep 26 17:35:45 1994 +0100 (1994-09-26)
changeset 61897b715e65f70
parent 617 94436ad4b60d
child 619 a0342b27b38e
added init_database (somewhat experimental);
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Mon Sep 26 17:35:23 1994 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Mon Sep 26 17:35:45 1994 +0100
     1.3 @@ -60,20 +60,17 @@
     1.4                               and Tactical=Tactical and Net=Net);
     1.5  structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
     1.6                             and Tactic=Tactic and Pattern=Pattern);
     1.7 -structure AxClass = AxClassFun(structure Logic = Logic 
     1.8 +structure AxClass = AxClassFun(structure Logic = Logic
     1.9    and Goals = Goals and Tactic = Tactic);
    1.10  open BasicSyntax Thm Drule Tactical Tactic Goals AxClass;
    1.11  
    1.12  structure Pure = struct val thy = pure_thy end;
    1.13  
    1.14 -use "install_pp.ML";
    1.15 -
    1.16 -
    1.17 -
    1.18 -(*Theory parser
    1.19 -  (The new Thy/read.ML needs Thm so this has to be done AFTER Thm is
    1.20 -   created.) *)
    1.21 +(*Theory parser and loader*)
    1.22  cd "Thy";
    1.23  use "ROOT.ML";
    1.24  cd "..";
    1.25  
    1.26 +use "install_pp.ML";
    1.27 +fun init_database () = (init_thy_reader (); init_pps ());
    1.28 +