src/HOL/IMP/ROOT.ML
changeset 4449 df30e75f670f
parent 1696 e84bff5c519b
child 6349 f7750d816c21
--- a/src/HOL/IMP/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/IMP/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -7,7 +7,7 @@
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/IMP";
-proof_timing := true;
+set proof_timing;
 time_use_thy "Expr";
 time_use_thy "Transition";
 time_use_thy "VC";