--- a/src/HOL/W0/Type.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/Type.ML Sat Mar 07 16:29:29 1998 +0100
@@ -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() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
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() addsplits [expand_if])) 1);
+by (fast_tac (set_cs addss simpset()) 1);
qed_spec_mp "ftv_mem_sub_ftv_list";
Addsimps [ftv_mem_sub_ftv_list];