src/HOL/Auth/NS_Public.ML

--- a/src/HOL/Auth/NS_Public.ML	Tue Sep 16 13:58:02 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Tue Sep 16 14:04:10 1997 +0200
@@ -124,8 +124,7 @@
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
-              (!simpset addsimps [not_parts_not_analz]
-                        setloop split_tac [expand_if]));
+              (!simpset setloop split_tac [expand_if]));
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)