src/HOL/Library/Mapping.thy

--- a/src/HOL/Library/Mapping.thy	Wed Jul 13 15:23:33 2016 +0200
+++ b/src/HOL/Library/Mapping.thy	Wed Jul 13 19:02:23 2016 +0200
@@ -74,11 +74,11 @@
       (\<lambda>k. if k < length xs then Some (xs ! k) else None)
       (\<lambda>k. if k < length ys then Some (ys ! k) else None)"
     apply induct
-    apply auto
+     apply auto
     unfolding rel_fun_def
     apply clarsimp
     apply (case_tac xa)
-    apply (auto dest: list_all2_lengthD list_all2_nthD)
+     apply (auto dest: list_all2_lengthD list_all2_nthD)
     done
 qed