src/Cube/ROOT.ML
changeset 3511 da4dd8b7ced4
parent 2237 f01ac387e82b
child 3941 ea440c63d206
--- a/src/Cube/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/Cube/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -1,20 +1,18 @@
-(*  Title:      Cube/ROOT
+(*  Title:      Cube/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
-The Lambda-Cube a la Barendregt
+The Lambda-Cube a la Barendregt.
 *)
 
 val banner = "Barendregt's Lambda-Cube";
 writeln banner;
 
-init_thy_reader();
+print_depth 1;  
 
-print_depth 1;  
 use_thy "Cube";
 
-init_pps ();
 print_depth 8;
 
 val Cube_build_completed = ();  (*indicate successful build*)