diff -r c5232e6fb10b -r 3fb16bed5d6c src/HOL/Data_Structures/RBT_Map.thy
--- a/src/HOL/Data_Structures/RBT_Map.thy	Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/RBT_Map.thy	Wed Sep 25 17:22:57 2019 +0200
@@ -24,7 +24,7 @@
 
 fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" where
 "del x Leaf = Leaf" |
-"del x (Node l (a,b) c r) = (case cmp x a of
+"del x (Node l ((a,b), c) r) = (case cmp x a of
      LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
            then baldL (del x l) (a,b) r else R (del x l) (a,b) r |
      GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black