diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -36,7 +36,7 @@
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (!simpset addsimps [imageI, spies_Cons]
-	                setloop split_tac [expand_event_case, expand_if])));
+	                addsplits [expand_event_case, expand_if])));
 qed "Spy_spies_bad";
 
 AddSIs [Spy_spies_bad];
@@ -111,7 +111,7 @@
 by (res_inst_tac [("x","0")] exI 1);
 by (ALLGOALS (asm_simp_tac
 	      (!simpset addsimps [used_Cons]
-			setloop split_tac [expand_event_case, expand_if])));
+			addsplits [expand_event_case, expand_if])));
 by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
@@ -238,7 +238,7 @@
                          insert_Key_singleton, subset_Compl_range,
                          Key_not_used, insert_Key_image, Un_assoc RS sym]
                         @disj_comms)
-              setloop split_tac [expand_if];
+              addsplits [expand_if];
 
 (*Lemma for the trivial direction of the if-and-only-if*)
 goal thy