src/HOL/Auth/TLS.ML

 fun analz_induct_tac i = 
     etac tls.induct i   THEN
     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     ALLGOALS (asm_simp_tac 
               (simpset() addcongs [if_weak_cong]
-                         addsimps (expand_ifs@pushes)))  THEN
+                         addsimps (split_ifs@pushes)))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
     ALLGOALS (asm_simp_tac 
               (simpset() addcongs [if_weak_cong]
 			 addsimps [insert_absorb]));

 by (ClientKeyExch_tac 7);
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_keys_lemma));
 by (ALLGOALS    (*18 seconds*)
     (asm_simp_tac (analz_image_keys_ss 
-		   addsimps (expand_ifs@pushes)
+		   addsimps (split_ifs@pushes)
 		   addsimps [range_sessionkeys_not_priK, 
                              analz_image_priK, certificate_def])));
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
 (*Fake*) 
 by (spy_analz_tac 1);