src/HOL/Auth/Yahalom.ML

 \         Key K ~: analz (spies evs)";
 by (etac yahalom.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (simpset() addsimps (split_ifs@pushes)
-	        addsimps [analz_insert_eq, analz_insert_freshK])));
+     (simpset() addsimps split_ifs @ pushes @
+                         [analz_insert_eq, analz_insert_freshK])));
 (*Oops*)
 by (blast_tac (claset() addDs [unique_session_keys]) 3);
 (*YM3*)
 by (blast_tac (claset() delrules [impCE]
                         addSEs spies_partsEs

 \  Nonce NB ~: analz (spies evs)";
 by (etac yahalom.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (simpset() addsimps (split_ifs@pushes)
-	        addsimps [analz_insert_eq, analz_insert_freshK])));
+     (simpset() addsimps split_ifs @ pushes @
+	                 [analz_insert_eq, analz_insert_freshK])));
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
 	                addSEs [MPair_parts]
 		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
     THEN flexflex_tac);