# HG changeset patch
# User wenzelm
# Date 780597345 -3600
# Node ID 97b715e65f7047bff170425019dc6b1fa8be7db9
# Parent  94436ad4b60d53f1bbd4d4c56a7b944e3d3f2ef7
added init_database (somewhat experimental);

diff -r 94436ad4b60d -r 97b715e65f70 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 26 17:35:23 1994 +0100
+++ b/src/Pure/ROOT.ML	Mon Sep 26 17:35:45 1994 +0100
@@ -60,20 +60,17 @@
                              and Tactical=Tactical and Net=Net);
 structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
                            and Tactic=Tactic and Pattern=Pattern);
-structure AxClass = AxClassFun(structure Logic = Logic 
+structure AxClass = AxClassFun(structure Logic = Logic
   and Goals = Goals and Tactic = Tactic);
 open BasicSyntax Thm Drule Tactical Tactic Goals AxClass;
 
 structure Pure = struct val thy = pure_thy end;
 
-use "install_pp.ML";
-
-
-
-(*Theory parser
-  (The new Thy/read.ML needs Thm so this has to be done AFTER Thm is
-   created.) *)
+(*Theory parser and loader*)
 cd "Thy";
 use "ROOT.ML";
 cd "..";
 
+use "install_pp.ML";
+fun init_database () = (init_thy_reader (); init_pps ());
+