src/HOL/Library/RBT_Set.thy

 lemma [code, code del]:
   "Ball = Ball" ..
 
 lemma [code, code del]:
   "Bex = Bex" ..
-
-term can_select
 
 lemma [code, code del]:
   "can_select = can_select" ..
 
 lemma [code, code del]:

 
 section {* Code equations *}
 
 code_datatype Set Coset
 
+declare set.simps[code]
+
 lemma empty_Set [code]:
   "Set.empty = Set RBT.empty"
 by (auto simp: Set_def)
 
 lemma UNIV_Coset [code]: