src/HOL/Auth/Yahalom2.ML

--- a/src/HOL/Auth/Yahalom2.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -227,7 +227,7 @@
 by (ALLGOALS
     (asm_simp_tac 
      (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
-               setloop split_tac [expand_if])));
+               addsplits [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 3);
 (*YM3*)