diff -r a3de7f32728c -r fe79ad367d77 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/W0/W.ML	Thu May 15 15:51:47 1997 +0200
@@ -45,7 +45,7 @@
         "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
-by (fast_tac (HOL_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (HOL_cs addss(!simpset setloop (split_tac [expand_if]))) 1);
 (* case Abs e *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -91,7 +91,7 @@
 \                 new_tv m s & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs addDs [list_all_nth] unsafe_addss (!simpset 
+by (fast_tac (HOL_cs addDs [list_all_nth] addss (!simpset 
         addsimps [id_subst_def,new_tv_list,new_tv_subst] 
         setloop (split_tac [expand_if]))) 1);
 (* case Abs e *)
@@ -160,7 +160,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
-    unsafe_addss (!simpset setloop (split_tac [expand_if]))) 1);
+    addss (!simpset setloop (split_tac [expand_if]))) 1);
 
 (* case Abs e *)
 by (asm_full_simp_tac (!simpset addsimps