# HG changeset patch
# User nipkow
# Date 1448018570 -3600
# Node ID e77cb3792503a0afd62f887b185c50ab77264af4
# Parent  4de2380ae3ab3ca87b5a3680c2d0aa1128c53742# Parent  47f7263870a0569c75e416ef4640bef32f0e683f
merged

diff -r 4de2380ae3ab -r e77cb3792503 src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Thu Nov 19 16:03:10 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Fri Nov 20 12:22:50 2015 +0100
@@ -36,7 +36,7 @@
 
 fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" 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 tree234 \<Rightarrow> 'a up\<^sub>i" where
 "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
@@ -97,8 +97,8 @@
 datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
 
 fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" 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"
 
 fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
 "node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" |
diff -r 4de2380ae3ab -r e77cb3792503 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 19 16:03:10 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Nov 20 12:22:50 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 *)