removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
--- a/src/HOL/Library/Executable_Set.thy Mon Oct 03 15:39:30 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy Mon Oct 03 22:21:19 2011 +0200
@@ -124,6 +124,9 @@
"Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
by (simp add: list_ex_iff)
+lemma
+ [code, code del]: "card S = card S" ..
+
lemma card_Set [code]:
"card (Set xs) = length (remdups xs)"
proof -