diff -r c7869a443b14 -r f01ac387e82b src/Cube/ROOT.ML --- 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*)