src/Pure/ROOT.ML
changeset 3508 089806e6133b
parent 3280 87e734c72152
child 3763 31ec17820f49
     1.1 --- a/src/Pure/ROOT.ML	Wed Jul 09 12:57:04 1997 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Jul 09 16:52:51 1997 +0200
     1.3 @@ -55,5 +55,5 @@
     1.4  cd "..";
     1.5  
     1.6  use "install_pp.ML";
     1.7 -fun init_database () = (init_thy_reader (); init_pps ());
     1.8  
     1.9 +print_depth 8;