removed init_database;
authorwenzelm
Wed Jul 09 16:52:51 1997 +0200 (1997-07-09)
changeset 3508089806e6133b
parent 3507 157be29ad5ba
child 3509 db03a42120bf
removed init_database;
src/Pure/ROOT.ML
     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;