# HG changeset patch
# User wenzelm
# Date 868459971 -7200
# Node ID 089806e6133b6f89f69d37b68a937e582f1fbad9
# Parent  157be29ad5ba132356a6e8f0c0a46386a76f865e
removed init_database;

diff -r 157be29ad5ba -r 089806e6133b 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;