src/Cube/ROOT.ML
changeset 2237 f01ac387e82b
parent 1459 d12da312eff4
child 3511 da4dd8b7ced4
--- a/src/Cube/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
+++ b/src/Cube/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
@@ -14,7 +14,7 @@
 print_depth 1;  
 use_thy "Cube";
 
-use "../Pure/install_pp.ML";
+init_pps ();
 print_depth 8;
 
 val Cube_build_completed = ();  (*indicate successful build*)