--- a/src/HOL/Library/AList.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Library/AList.thy Sun Nov 20 21:05:23 2011 +0100
@@ -467,7 +467,7 @@
(map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
by (simp add: merge_conv' map_add_Some_iff)
-lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
+lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
by (simp add: merge_conv')