diff -r 6bf8ea65ea7a -r facaf96cd79e src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Tue Jan 29 17:33:40 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Tue Jan 29 13:54:43 2019 +0100
@@ -183,10 +183,10 @@
 fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "del_hi n Leaf = Leaf" |
 "del_hi n (Node l x r) =
-	(if n = 1 then Leaf
-	 else if even n
-	     then Node (del_hi (n div 2) l) x r
-	     else Node l x (del_hi (n div 2) r))"
+  (if n = 1 then Leaf
+   else if even n
+       then Node (del_hi (n div 2) l) x r
+       else Node l x (del_hi (n div 2) r))"
 
 
 subsubsection "Functional Correctness"