diff -r d5ddd022a451 -r 47f7263870a0 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 19 22:35:10 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Nov 20 12:22:41 2015 +0100
@@ -30,7 +30,7 @@
 
 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" |
@@ -72,8 +72,8 @@
 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 *)