diff -r ed8d50969995 -r a31a9da43694 src/HOL/Data_Structures/RBT_Map.thy
--- a/src/HOL/Data_Structures/RBT_Map.thy	Thu Feb 20 09:05:19 2020 +0100
+++ b/src/HOL/Data_Structures/RBT_Map.thy	Fri Feb 21 17:51:56 2020 +0100
@@ -29,7 +29,7 @@
            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
            then baldR l (a,b) (del x r) else R l (a,b) (del x r) |
-  EQ \<Rightarrow> combine l r)"
+  EQ \<Rightarrow> app l r)"
 
 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
 "delete x t = paint Black (del x t)"
@@ -49,7 +49,7 @@
 lemma inorder_del:
  "sorted1(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
 by(induction x t rule: del.induct)
-  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
+  (auto simp: del_list_simps inorder_app inorder_baldL inorder_baldR)
 
 lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
@@ -86,7 +86,7 @@
   thus ?case proof (elim disjE)
     assume "x = y"
     with 2 show ?thesis
-    by (cases c) (simp_all add: invh_combine invc_combine)
+    by (cases c) (simp_all add: invh_app invc_app)
   next
     assume "x < y"
     with 2 show ?thesis