src/FOL/ex/ROOT.ML
changeset 4446 097004a470fb
parent 2601 b301958c465d
child 6349 f7750d816c21
--- a/src/FOL/ex/ROOT.ML	Fri Dec 19 10:17:04 1997 +0100
+++ b/src/FOL/ex/ROOT.ML	Fri Dec 19 10:18:03 1997 +0100
@@ -10,7 +10,7 @@
 
 FOL_build_completed;    (*Cause examples to fail if FOL did*)
 
-proof_timing := true;
+set proof_timing;
 
 time_use     "intro.ML";
 time_use_thy "Nat";
@@ -39,7 +39,3 @@
 
 writeln"\n** How to declare an oracle **\n";
 time_use_thy "IffOracle";
-
-
-OS.FileSys.chDir "..";
-maketest"END: Root file for FOL examples";