--- a/src/HOL/Auth/KerberosIV.ML Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Auth/KerberosIV.ML Tue May 30 16:08:38 2000 +0200
@@ -7,7 +7,7 @@
*)
Pretty.setdepth 20;
-proof_timing:=true;
+set timing;
AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];