# HG changeset patch
# User bulwahn
# Date 1317673279 -7200
# Node ID 717bc892e4d7cb512d84761b5a766b1a632b701a
# Parent  055c6ff9c5c3502ff884ad0e300e4df356f4605a
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++

diff -r 055c6ff9c5c3 -r 717bc892e4d7 src/HOL/Library/Executable_Set.thy
--- 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 -