src/HOL/BCV/Orders.ML
changeset 8288 ebf874fcbff2
parent 7961 422ac6888c7f
child 8423 3c19160b6432
--- 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];