diff -r 8050734eee3e -r 9660bbf5ce7e src/HOL/Data_Structures/Array_Braun.thy --- a/src/HOL/Data_Structures/Array_Braun.thy Tue Oct 30 16:24:04 2018 +0100 +++ b/src/HOL/Data_Structures/Array_Braun.thy Tue Oct 30 18:11:22 2018 +0100 @@ -266,11 +266,11 @@ subsection "Faster" -fun braun_of_rec :: "'a \ nat \ 'a tree" where -"braun_of_rec x n = (if n=0 then Leaf +fun braun_of_naive :: "'a \ nat \ 'a tree" where +"braun_of_naive x n = (if n=0 then Leaf else let m = (n-1) div 2 - in if odd n then Node (braun_of_rec x m) x (braun_of_rec x m) - else Node (braun_of_rec x (m + 1)) x (braun_of_rec x m))" + in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m) + else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))" fun braun2_of :: "'a \ nat \ 'a tree * 'a tree" where "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)