src/Pure/ROOT.ML
changeset 3508 089806e6133b
parent 3280 87e734c72152
child 3763 31ec17820f49
--- 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;