--- a/src/HOL/W0/Type.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/W0/Type.ML Fri Oct 17 15:25:12 1997 +0200
@@ -157,7 +157,7 @@
goal thy
"new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
by (typ.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
qed "subst_te_new_tv";
Addsimps [subst_te_new_tv];
@@ -259,7 +259,7 @@
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
-by (fast_tac (set_cs addss(!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (set_cs addss(!simpset addsplits [expand_if])) 1);
qed_spec_mp "ftv_mem_sub_ftv_list";
Addsimps [ftv_mem_sub_ftv_list];