src/HOL/Auth/Shared.ML

 (*Spy sees shared keys of agents!*)
 goal thy "!!A. A: bad ==> Key (shrK A) : spies evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [imageI, spies_Cons]
-	                addsplits [expand_event_case, expand_if])));
+	                addsplits [expand_event_case])));
 qed "Spy_spies_bad";
 
 AddSIs [Spy_spies_bad];
 
 (*For not_bad_tac*)

 goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
 by (induct_tac "evs" 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [used_Cons]
-			addsplits [expand_event_case, expand_if])));
+			addsplits [expand_event_case])));
 by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
 val lemma = result();
 

               delsimps [imp_disjL]    (*reduces blow-up*)
               addsimps ([image_insert RS sym, image_Un RS sym,
                          analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
                          insert_Key_singleton, subset_Compl_range,
                          Key_not_used, insert_Key_image, Un_assoc RS sym]
-                        @disj_comms)
-              addsplits [expand_if];
+                        @disj_comms);
 
 (*Lemma for the trivial direction of the if-and-only-if*)
 goal thy  
  "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
 \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";