--- a/src/HOL/BCV/Orders.ML Thu Feb 24 08:55:37 2000 +0100
+++ b/src/HOL/BCV/Orders.ML Thu Feb 24 08:56:36 2000 +0100
@@ -147,7 +147,7 @@
Goalw [listsn_def]
"[| xs : listsn n A; x:A; i < n |] ==> xs[i := x] : listsn n A";
by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addDs [set_list_update_subset RS subsetD]) 1);
+by (blast_tac (claset() addDs [set_update_subset_insert RS subsetD]) 1);
qed "list_update_in_listsn";
Addsimps [list_update_in_listsn];
AddSIs [list_update_in_listsn];
--- a/src/HOL/MicroJava/BV/Correct.ML Thu Feb 24 08:55:37 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML Thu Feb 24 08:56:36 2000 +0100
@@ -114,7 +114,7 @@
Goalw [approx_loc_def,list_all2_def]
"\\<forall>loc idx x X. (approx_loc G hp loc LT) \\<longrightarrow> (approx_val G hp x X) \
\ \\<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))";
-by (fast_tac (claset() addDs [set_update_subset RS subsetD]
+by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD]
addss (simpset() addsimps [zip_update])) 1);
qed_spec_mp "approx_loc_imp_approx_loc_subst";