--- a/src/HOL/Map.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Map.ML Sat Mar 07 16:29:29 1998 +0100
@@ -21,7 +21,7 @@
qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
(K [Asm_simp_tac 1]);
qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
- (K [rtac ext 1, asm_simp_tac (simpset() addsplits [expand_if]) 1]);
+ (K [rtac ext 1, Asm_simp_tac 1]);
(*Addsimps [update_same, update_other, update_triv];*)
section "++";
@@ -56,14 +56,14 @@
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (rtac ext 1);
-by (asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
qed "map_of_append";
Addsimps [map_of_append];
goal thy "map_of xs k = Some y --> (k,y):set xs";
by (list.induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
by (split_all_tac 1);
by (Simp_tac 1);
qed_spec_mp "map_of_SomeD";
@@ -76,7 +76,7 @@
Addsimps [dom_empty];
goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "dom_update";
Addsimps [dom_update];