diff -r d7393c35aa5d -r 976d656ed31e src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Thu Dec 03 23:00:23 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Fri Dec 04 13:24:49 2020 +0100
@@ -98,14 +98,14 @@
 
 subsection \<open>Balancedness\<close>
 
-lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> height(upd x y t) = height t"
+lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> hI(upd x y t) = height t"
 by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *)
 
 corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
 by (simp add: update_def complete_upd)
 
 
-lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> hD(del x t) = height t"
 by(induction x t rule: del.induct)
   (auto simp add: heights max_def height_split_min split: prod.split)