src/HOL/Data_Structures/AVL_Set.thy

--- a/src/HOL/Data_Structures/AVL_Set.thy	Tue Aug 20 12:19:23 2019 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Aug 20 15:42:23 2019 +0200
@@ -134,7 +134,7 @@
 declare Let_def [simp]
 
 lemma ht_height[simp]: "avl t \<Longrightarrow> ht t = height t"
-by (induct t) simp_all
+by (cases t) simp_all
 
 lemma height_balL:
   "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>