# HG changeset patch
# User wenzelm
# Date 1407080339 -7200
# Node ID 34382a1f37d61962a708a4e00036349b3d6ebd78
# Parent  6d8f97d555d84ab94e2fbe988aa45bfeb737d9c7
tuned whitespace;

diff -r 6d8f97d555d8 -r 34382a1f37d6 src/HOL/Library/AList_Mapping.thy
--- 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]: