removed init_database;
authorwenzelm
Wed, 09 Jul 1997 16:52:51 +0200
changeset 3508 089806e6133b
parent 3507 157be29ad5ba
child 3509 db03a42120bf
removed init_database;
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jul 09 12:57:04 1997 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 09 16:52:51 1997 +0200
@@ -55,5 +55,5 @@
 cd "..";
 
 use "install_pp.ML";
-fun init_database () = (init_thy_reader (); init_pps ());
 
+print_depth 8;