diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -808,7 +808,7 @@
 by analz_sees_tac;
 by (ALLGOALS 
     (asm_simp_tac 
-     (simpset() addsimps ([Says_Kas_message_form, 
+     (simpset() addsimps ([Says_Kas_message_form, less_SucI,
 			   analz_insert_eq, not_parts_not_analz, 
 			   analz_insert_freshK1] @ pushes))));
 (*Fake*) 
@@ -868,9 +868,11 @@
 by (rotate_tac ~1 11);
 by (ALLGOALS 
     (asm_full_simp_tac 
-     (simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form,
-			   analz_insert_eq, not_parts_not_analz, 
-			   analz_insert_freshK1, analz_insert_freshK2] @ pushes))));
+     (simpset() addsimps [less_SucI, 
+			  Says_Kas_message_form, Says_Tgs_message_form,
+			  analz_insert_eq, not_parts_not_analz, 
+			  analz_insert_freshK1, analz_insert_freshK2] 
+			 @ pushes)));
 (*Fake*) 
 by (spy_analz_tac 1);
 (*K2*)