--- 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