src/HOL/Auth/OtwayRees_Bad.ML

 by (etac otway.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong] 
                             addsimps [analz_insert_eq, analz_insert_freshK]
-                            setloop split_tac [expand_if])));
+                            addsplits [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
 (*OR4*) 
 by (Blast_tac 3);
 (*OR3*)