diff -r ae683a461c40 -r 16fab31feadc src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Aug 06 23:46:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Aug 07 11:46:14 2020 +0200
@@ -299,7 +299,7 @@
   case 2
   then show ?case by (simp add: \<phi>_def real_le_lsqrt)
 next
-  case (3 n) term ?case
+  case (3 n)
   have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n"
     by (simp add: field_simps power2_eq_square)
   also have "\<dots> = (\<phi> + 1) * \<phi> ^ n"