src/HOL/Data_Structures/Tree23_Set.thy

 
 datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
 
 fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
 "tree\<^sub>i (T\<^sub>i t) = t" |
-"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
+"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
 
 fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
 "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
 "ins x (Node2 l a r) =
    (case cmp x a of

 "insert x t = tree\<^sub>i(ins x t)"
 
 datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
 
 fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
-"tree\<^sub>d (T\<^sub>d x) = x" |
-"tree\<^sub>d (Up\<^sub>d x) = x"
+"tree\<^sub>d (T\<^sub>d t) = t" |
+"tree\<^sub>d (Up\<^sub>d t) = t"
 
 (* Variation: return None to signal no-change *)
 
 fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
 "node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |