--- a/src/HOL/Library/RBT_Set.thy Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/Library/RBT_Set.thy Wed Feb 19 16:32:37 2014 +0100
@@ -520,7 +520,7 @@
code_datatype Set Coset
-declare set.simps[code]
+declare set_simps[code]
lemma empty_Set [code]:
"Set.empty = Set RBT.empty"