1.1 --- a/src/HOL/Library/AList_Mapping.thy	Sun Aug 03 17:33:38 2014 +0200
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Sun Aug 03 17:38:59 2014 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4    have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
     1.5      by (auto simp add: image_def intro!: bexI)
     1.6    show ?thesis apply transfer
     1.7 -  by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
     1.8 +    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
     1.9  qed
    1.10  
    1.11  lemma [code nbe]: