src/HOL/Auth/TLS.ML
changeset 3919 c036caebfc75
parent 3772 6ee707a73248
child 3961 6a8996fb7d99
--- a/src/HOL/Auth/TLS.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -146,7 +146,7 @@
     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
@@ -198,13 +198,13 @@
     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 ***)