diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu May 15 15:51:47 1997 +0200
@@ -140,7 +140,7 @@
 by (Step_tac 1);
 by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
 by (ALLGOALS
-    (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
+    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
 				            setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Says";
 
@@ -157,7 +157,7 @@
  "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
 \        ==> X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      unsafe_addss (!simpset)) 1);
+                      addss (!simpset)) 1);
 qed "Says_Crypt_lost";
 
 goal thy  
@@ -165,7 +165,7 @@
 \           X ~: analz (sees lost Spy evs) |]                     \
 \        ==> C ~: lost";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      unsafe_addss (!simpset)) 1);
+                      addss (!simpset)) 1);
 qed "Says_Crypt_not_lost";
 
 (*NEEDED??*)