src/HOL/Auth/TLS.ML

     etac tls.induct i
     THEN 
     REPEAT (FIRSTGOAL analz_mono_contra_tac)
     THEN 
     fast_tac (!claset addss (!simpset)) i THEN
-    ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
+    ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
 
 
 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
     sends messages containing X! **)
 

 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]
-                        setloop split_tac [expand_if]))  THEN
+                        addsplits [expand_if]))  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]
-                        setloop split_tac [expand_if]));
+                        addsplits [expand_if]));
 
 
 (*** Properties of items found in Notes ***)
 
 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \