diff -r f90874d3a246 -r c8e3cf3520b3 src/HOL/Codegenerator_Test/RBT_Set_Test.thy
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Fri Feb 15 09:41:25 2013 +0100
@@ -25,9 +25,17 @@
 lemma [code, code del]:
   "acc = acc" ..
 
-lemmas [code del] =
-  finite_set_code finite_coset_code 
-  equal_set_code
+lemma [code, code del]:
+  "Cardinality.card' = Cardinality.card'" ..
+
+lemma [code, code del]:
+  "Cardinality.finite' = Cardinality.finite'" ..
+
+lemma [code, code del]:
+  "Cardinality.subset' = Cardinality.subset'" ..
+
+lemma [code, code del]:
+  "Cardinality.eq_set = Cardinality.eq_set" ..
 
 (*
   If the code generation ends with an exception with the following message: