diff -r 36e58620ffc8 -r 26685edee372 src/HOL/Auth/KerberosIV.ML
--- 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];