src/HOL/Auth/NS_Public_Bad.ML

--- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -122,7 +122,7 @@
 (*Tactic for proving secrecy theorems*)
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
-    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+    ALLGOALS Asm_simp_tac;
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)