diff -r 761af5c2fd59 -r 6e62e5357a10 src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Sat Apr 26 12:38:42 2003 +0200
@@ -177,7 +177,7 @@
 \     Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
 by (parts_induct_tac 1);
 (*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
+by (force_tac (claset() addSDs [keysFor_parts_insert], simpset()) 1);
 (*Others*)
 by (ALLGOALS Blast_tac);
 qed_spec_mp "new_keys_not_used";