--- 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 ***)