--- a/src/HOL/Library/RBT_Impl.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -45,7 +45,7 @@
 definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where
   "keys t = map fst (entries t)"
 
-lemma keys_simps [simp, code]:
+lemma keys_simps [simp]:
   "keys Empty = []"
   "keys (Branch c l k v r) = keys l @ k # keys r"
   by (simp_all add: keys_def)