--- a/src/HOL/Auth/KerberosIV.ML Tue Aug 17 22:13:23 1999 +0200
+++ b/src/HOL/Auth/KerberosIV.ML Tue Aug 17 22:14:02 1999 +0200
@@ -8,7 +8,6 @@
Pretty.setdepth 20;
proof_timing:=true;
-HOL_quantifiers := false;
AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];