src/HOL/Auth/NS_Shared.ML

 by (etac ns_shared.induct 1);
 by analz_spies_tac;
 by (ALLGOALS 
     (asm_simp_tac 
      (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
-               setloop split_tac [expand_if])));
+               addsplits [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 5);
 (*NS3, replay sub-case*) 
 by (Blast_tac 4);
 (*NS2*)