# HG changeset patch
# User nipkow
# Date 1540919482 -3600
# Node ID 9660bbf5ce7e85ee0cf9e185242d259d2504fdf0
# Parent  8050734eee3ee3b314962bfb02e978f85f3dba17
tuned name

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 \<Rightarrow> nat \<Rightarrow> 'a tree" where
-"braun_of_rec x n = (if n=0 then Leaf
+fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> '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 \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
 "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)