--- a/src/HOL/Auth/TLS.ML Mon Jan 12 15:47:43 1998 +0100
+++ b/src/HOL/Auth/TLS.ML Mon Jan 12 16:56:39 1998 +0100
@@ -299,7 +299,6 @@
\ ==> Nonce PMS : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [parts_insert_spies])));
by (Fake_parts_insert_tac 1);
(*Six others, all trivial or by freshness*)
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]
@@ -446,7 +445,6 @@
(*SpyKeys*)
by (blast_tac (claset() addSEs spies_partsEs) 3);
(*Fake*)
-by (simp_tac (simpset() addsimps [parts_insert_spies]) 2);
by (Fake_parts_insert_tac 2);
(** LEVEL 6 **)
(*Oops*)