diff -r cf86e095a439 -r 92afc125f7cd src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Thu May 29 14:18:27 2025 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Fri May 30 07:47:03 2025 +0200
@@ -29,7 +29,7 @@
 
 declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set
   Set.member Set.insert Set.remove UNIV Set.filter image
-  Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter
+  Set.subset_eq Ball Bex Set.can_select Set.union minus_set_inst.minus_set Set.inter
   card the_elem Pow sum prod Product_Type.product Id_on
   Image trancl relcomp wf_on wf_code Min Inf_fin Max Sup_fin
   "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"