src/HOL/Auth/Kerberos_BAN.thy

--- a/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 20 12:09:33 2007 +0200
@@ -133,7 +133,7 @@
 apply (rule_tac [2]
            bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
                              THEN bankerberos.BK3, THEN bankerberos.BK4])
-apply (possibility, simp_all (no_asm_simp) add: used_Cons)
+apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
 done
 
 subsection{*Lemmas for reasoning about predicate "Issues"*}