src/HOL/Library/AList_Mapping.thy
changeset 57850 34382a1f37d6
parent 51161 6ed12ae3b3e1
child 58881 b9556a055632
--- a/src/HOL/Library/AList_Mapping.thy	Sun Aug 03 17:33:38 2014 +0200
+++ b/src/HOL/Library/AList_Mapping.thy	Sun Aug 03 17:38:59 2014 +0200
@@ -60,7 +60,7 @@
   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]: