src/HOL/Auth/Shared.ML

 bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
 Addsimps [invKey_shrK, invKey_newK];
 
 
 (*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
+AddIffs [inj_shrK RS inj_eq];
+AddSDs  [newN_length, newK_length];
 
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
 
 Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];