src/HOL/Library/AList_Mapping.thy

     in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
 proof -
   have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
     by (auto simp add: image_def intro!: bexI)
   show ?thesis apply transfer
-  by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
+    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
 qed
 
 lemma [code nbe]:
   "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
   by (fact equal_refl)