src/HOL/Data_Structures/Tree23_Set.thy
changeset 61709 47f7263870a0
parent 61678 b594e9277be3
child 62130 90a3016a6c12
     1.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 19 22:35:10 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Nov 20 12:22:41 2015 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
     1.6  "tree\<^sub>i (T\<^sub>i t) = t" |
     1.7 -"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
     1.8 +"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
     1.9  
    1.10  fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
    1.11  "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    1.12 @@ -72,8 +72,8 @@
    1.13  datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
    1.14  
    1.15  fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
    1.16 -"tree\<^sub>d (T\<^sub>d x) = x" |
    1.17 -"tree\<^sub>d (Up\<^sub>d x) = x"
    1.18 +"tree\<^sub>d (T\<^sub>d t) = t" |
    1.19 +"tree\<^sub>d (Up\<^sub>d t) = t"
    1.20  
    1.21  (* Variation: return None to signal no-change *)
    1.22