diff -r de74b549f976 -r 097004a470fb src/Cube/ex/ROOT.ML
--- a/src/Cube/ex/ROOT.ML	Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Cube/ex/ROOT.ML	Fri Dec 19 10:18:03 1997 +0100
@@ -2,9 +2,6 @@
 writeln"Root file for Cube examples";
 Cube_build_completed;    (*Cause examples to fail if Cube did*)
 
-proof_timing := true;
+set proof_timing;
 
-use"ex.ML";
-
-cd "..";
-maketest"END: file for Lambda-Cube examples";
+use "ex.ML";