--- a/src/HOL/Data_Structures/RBT_Map.thy Mon Jun 11 08:15:43 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Map.thy Mon Jun 11 16:29:27 2018 +0200
@@ -27,7 +27,7 @@
and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
where
"del x Leaf = Leaf" |
-"del x (Node c t1 (a,b) t2) = (case cmp x a of
+"del x (Node t1 (a,b) c t2) = (case cmp x a of
LT \<Rightarrow> delL x t1 (a,b) t2 |
GT \<Rightarrow> delR x t1 (a,b) t2 |
EQ \<Rightarrow> combine t1 t2)" |