src/FOLP/ROOT.ML
changeset 3511 da4dd8b7ced4
parent 2237 f01ac387e82b
child 3836 f1a1817659e6
     1.1 --- a/src/FOLP/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     1.2 +++ b/src/FOLP/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     1.3 @@ -12,9 +12,8 @@
     1.4  
     1.5  writeln banner;
     1.6  
     1.7 -init_thy_reader();
     1.8 +print_depth 1;
     1.9  
    1.10 -print_depth 1;  
    1.11  use_thy "IFOLP";
    1.12  use_thy "FOLP";
    1.13  
    1.14 @@ -75,7 +74,7 @@
    1.15  
    1.16  use "simpdata.ML";
    1.17  
    1.18 -init_pps ();
    1.19 +
    1.20  print_depth 8;
    1.21  
    1.22  val FOLP_build_completed = ();  (*indicate successful build*)