src/HOL/Auth/Public.ML

--- a/src/HOL/Auth/Public.ML	Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Thu May 15 15:51:47 1997 +0200
@@ -120,7 +120,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";