--- a/src/HOL/Auth/TLS.ML Mon Apr 27 16:45:11 1998 +0200
+++ b/src/HOL/Auth/TLS.ML Mon Apr 27 16:45:27 1998 +0200
@@ -193,7 +193,7 @@
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
ALLGOALS (asm_simp_tac
(simpset() addcongs [if_weak_cong]
- addsimps (expand_ifs@pushes))) THEN
+ addsimps (split_ifs@pushes))) 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
@@ -405,7 +405,7 @@
by (REPEAT_FIRST (rtac analz_image_keys_lemma));
by (ALLGOALS (*18 seconds*)
(asm_simp_tac (analz_image_keys_ss
- addsimps (expand_ifs@pushes)
+ addsimps (split_ifs@pushes)
addsimps [range_sessionkeys_not_priK,
analz_image_priK, certificate_def])));
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));