diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/TLS.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -176,14 +176,10 @@
 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]
-                         addsimps split_ifs @ pushes))  THEN
+    ALLGOALS (asm_simp_tac (simpset() 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 
-              (simpset() addcongs [if_weak_cong]
-			 addsimps [insert_absorb]));
+    ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]));
 
 
 (*** Properties of items found in Notes ***)