diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Auth/KerberosIV.ML
--- 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];