diff -r d8363de26567 -r b56ed5010e69 src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 08:15:43 2018 +0200
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 16:29:27 2018 +0200
@@ -9,16 +9,16 @@
 begin
 
 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
-"update x y Leaf = Node 1 Leaf (x,y) Leaf" |
-"update x y (Node h l (a,b) r) = (case cmp x a of
-   EQ \<Rightarrow> Node h l (x,y) r |
+"update x y Leaf = Node Leaf (x,y) 1 Leaf" |
+"update x y (Node l (a,b) h r) = (case cmp x a of
+   EQ \<Rightarrow> Node l (x,y) h r |
    LT \<Rightarrow> balL (update x y l) (a,b) r |
    GT \<Rightarrow> balR l (a,b) (update x y r))"
 
 fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
 "delete _ Leaf = Leaf" |
-"delete x (Node h l (a,b) r) = (case cmp x a of
-   EQ \<Rightarrow> del_root (Node h l (a,b) r) |
+"delete x (Node l (a,b) h r) = (case cmp x a of
+   EQ \<Rightarrow> del_root (Node l (a,b) h r) |
    LT \<Rightarrow> balR (delete x l) (a,b) r |
    GT \<Rightarrow> balL l (a,b) (delete x r))"