src/HOL/Auth/TLS.ML
changeset 7057 b9ddbb925939
parent 6915 4ab8e31a8421
child 8054 2ce57ef2a4aa
--- a/src/HOL/Auth/TLS.ML	Wed Jul 21 15:20:26 1999 +0200
+++ b/src/HOL/Auth/TLS.ML	Wed Jul 21 15:22:11 1999 +0200
@@ -410,10 +410,10 @@
 by (blast_tac (claset() addIs [parts_insertI]) 2);
 (** LEVEL 6 **)
 (*Oops*)
-by (Force_tac 6);
 by (REPEAT 
-    (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
-				 Notes_master_imp_Crypt_PMS]) 1));
+    (force_tac (claset() addSDs [Notes_Crypt_parts_spies, 
+				 Notes_master_imp_Crypt_PMS],
+		simpset()) 1));
 val lemma = result();
 
 Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \