src/HOL/Library/RBT_Set.thy

--- a/src/HOL/Library/RBT_Set.thy	Fri Jan 25 16:45:09 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Tue Jan 15 12:13:27 2013 +0100
@@ -63,8 +63,6 @@
 lemma [code, code del]:
   "Bex = Bex" ..
 
-term can_select
-
 lemma [code, code del]:
   "can_select = can_select" ..
 
@@ -526,6 +524,8 @@
 
 code_datatype Set Coset
 
+declare set.simps[code]
+
 lemma empty_Set [code]:
   "Set.empty = Set RBT.empty"
 by (auto simp: Set_def)